Quelle  metric_space_def.prf

(metric_space_def
 (epsilon_net_subset1 0
  (epsilon_net_subset1-1 nil 3453921829 3453922018
   ("" (skosimp)
    (("" (expand "epsilon_net?")
      (("" (flatten)
        (("" (assert)
          (("" (split)
            (("1" (hide -1 -3) (("1" (grind) nil nil)) nil)
             ("2" (expand "subset?")
              (("2" (expand "member")
                (("2" (skosimp) (("2" (postpone) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil 80545 440 t shostak))
 (epsilon_net_subset2 0
  (epsilon_net_subset2-1 nil 3453922022 3453922847
   ("" (skosimp)
    (("" (expand "epsilon_net?")
      (("" (flatten)
        (("" (lemma "finite_subset" ("A" "Y!1" "s" "X!1"))
          (("1" (assert)
            (("1" (split)
              (("1" (hide -1 -2 -4) (("1" (grind) nil nil)) nil)
               ("2" (expand "subset?")
                (("2" (skosimp)
                  (("2" (expand "member")
                    (("2" (inst-cp -5 "x!1")
                      (("2" (assert)
                        (("2" (expand "image")
                          (("2" (expand "Union")
                            (("2" (skosimp)
                              (("2"
                                (typepred "a!1")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (replace -1)
                                    (("2"
                                      (typepred "x!2")
                                      (("2" (postpone) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil 825470 590 t shostak)))