:: TBSP_1  semantic presentation begin  























































theorem :: TBSP_1:1 (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k4_power :::"to_power"::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "L"))  ($#k4_power :::"to_power"::: )  (Set (Var "n")))))) ; 
 
theorem :: TBSP_1:2 (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "L"))  ($#k4_power :::"to_power"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "L"))  ($#k4_power :::"to_power"::: )  (Set (Var "k"))))  ")" ))) ; 
 
theorem :: TBSP_1:3 (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "L"))) & (Bool (Set (Var "L"))  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set (Var "L"))  ($#k4_power :::"to_power"::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "s")))))) ; 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; attr "N" is  :::"totally_bounded":::  means :: TBSP_1:def 1 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "N" "st"  (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "N")  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "G")))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "N"  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" "N" "st" (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "w")) "," (Set (Var "r")) ")" )))  ")" )  ")" ))); end; 




:: deftheorem    defines :::"totally_bounded"::: TBSP_1:def 1 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "N")) "is"   ($#v1_tbsp_1 :::"totally_bounded"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "N")) "st"  (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "G")))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "holds"  (Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st" (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "w")) "," (Set (Var "r")) ")" )))  ")" )  ")" )))  ")" )); 
 






theorem :: TBSP_1:4 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "N"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")))  ")" )  ")" )  ")" ))) ; 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; let "S2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "N")); attr "S2" is  :::"convergent":::  means :: TBSP_1:def 2 (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "N" "st"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set  "(" "S2"  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) "," (Set (Var "x")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))); end; 





:: deftheorem    defines :::"convergent"::: TBSP_1:def 2 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "S2")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "S2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) "," (Set (Var "x")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))))  ")" ))); 
 definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); let "S1" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "M")); assume 
(Bool (Set (Const "S1")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )
 ; func  :::"lim"::: "S1" ->   ($#m1_subset_1 :::"Element":::) "of" "M" means :: TBSP_1:def 3 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set  "(" "S1"  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) "," it ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))); end; 







:: deftheorem    defines :::"lim"::: TBSP_1:def 3 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "S1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tbsp_1 :::"lim"::: )  (Set (Var "S1")))) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "S1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) "," (Set (Var "b3")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" )))); 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; let "S2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "N")); attr "S2" is  :::"Cauchy":::  means :: TBSP_1:def 4 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set  "(" "S2"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" "S2"  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))); end; 





:: deftheorem    defines :::"Cauchy"::: TBSP_1:def 4 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "S2")) "is"   ($#v3_tbsp_1 :::"Cauchy"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "S2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "S2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" ))); 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; attr "N" is  :::"complete":::  means :: TBSP_1:def 5 (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" "N"  "st" (Bool (Bool (Set (Var "S2")) "is"   ($#v3_tbsp_1 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Var "S2")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )); end; 




:: deftheorem    defines :::"complete"::: TBSP_1:def 5 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "N")) "is"   ($#v4_tbsp_1 :::"complete"::: )  ) "iff" (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "S2")) "is"   ($#v3_tbsp_1 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Var "S2")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  ))  ")" )); 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; let "S2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "N")); let "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); :: original: :::"."::: redefine func "S2" :::"."::: "n" ->   ($#m1_subset_1 :::"Element":::) "of" "N"; end; 
theorem :: TBSP_1:5 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "N")) "is"   ($#v9_metric_1 :::"triangle"::: )  ) & (Bool (Set (Var "N")) "is"   ($#v8_metric_1 :::"symmetric"::: )  ) & (Bool (Set (Var "S2")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Var "S2")) "is"   ($#v3_tbsp_1 :::"Cauchy"::: )  ))) ; 
 registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M"))   ($#v2_tbsp_1 :::"convergent"::: )    ->   ($#v3_tbsp_1 :::"Cauchy"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M"))))); 
end; 
theorem :: TBSP_1:6 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_metric_1 :::"symmetric"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "S2")) "is"   ($#v3_tbsp_1 :::"Cauchy"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "S2"))  ($#k2_tbsp_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "k")) ")" ) ")" ) "," (Set  "(" (Set (Var "S2"))  ($#k2_tbsp_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" ))) ; 
 
theorem :: TBSP_1:7 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Contraction":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v4_tbsp_1 :::"complete"::: )  )) "holds"  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" )  ")" )))) ; 
 
theorem :: TBSP_1:8 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    "st" (Bool (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "T"))) "is"   ($#v1_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v4_tbsp_1 :::"complete"::: )  )) ; 
 
theorem :: TBSP_1:9 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    "st" (Bool (Bool (Set (Var "N")) "is"   ($#v6_metric_1 :::"Reflexive"::: )  ) & (Bool (Set (Var "N")) "is"   ($#v9_metric_1 :::"triangle"::: )  ) & (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "N"))) "is"   ($#v1_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set (Var "N")) "is"   ($#v1_tbsp_1 :::"totally_bounded"::: )  )) ; 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; attr "N" is  :::"bounded":::  means :: TBSP_1:def 6 (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "N" "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )  ")" )); let "C" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "N")); attr "C" is  :::"bounded":::  means :: TBSP_1:def 7 (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "N"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "C") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "C")) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )  ")" )); end; 









:: deftheorem    defines :::"bounded"::: TBSP_1:def 6 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "N")) "is"   ($#v5_tbsp_1 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N")) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )  ")" ))  ")" )); 
 
:: deftheorem    defines :::"bounded"::: TBSP_1:def 7 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )  ")" ))  ")" ))); 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k6_metric_1 :::"DiscreteSpace"::: )  "A") ->   ($#v5_tbsp_1 :::"bounded"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v7_metric_1 :::"discerning"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#v11_metric_1 :::"Discerning"::: )     ($#v5_tbsp_1 :::"bounded"::: )    for    ($#l1_metric_1 :::"MetrStruct"::: )  ; 
end; registrationlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v6_tbsp_1 :::"bounded"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "N"))); 
end; registrationlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster   ($#v6_tbsp_1 :::"bounded"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "N"))); 
end; 
theorem :: TBSP_1:10 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )) "implies" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "w")) "," (Set (Var "z")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )  ")" )))  ")"  &  "("  (Bool (Bool (Set (Var "N")) "is"   ($#v8_metric_1 :::"symmetric"::: )  ) & (Bool (Set (Var "N")) "is"   ($#v9_metric_1 :::"triangle"::: )  ) & (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)(Bool  "ex" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N")) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "w")) "," (Set (Var "z")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))  ")" )  ")" )))) "implies" (Bool (Set (Var "C")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )  ")"   ")" ))) ; 
 
theorem :: TBSP_1:11 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "N"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "N")) "is"   ($#v6_metric_1 :::"Reflexive"::: )  ) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "w")) "," (Set (Var "r")) ")" ))))) ; 
 
theorem :: TBSP_1:12 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "t1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "t1")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "t1" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k9_metric_1 :::"Ball"::: )   "(" "t1" "," "r" ")" ) ->   ($#v6_tbsp_1 :::"bounded"::: )   ; 
end; 
theorem :: TBSP_1:13 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "P")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set (Var "Q")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "P"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Q"))) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ))) ; 
 
theorem :: TBSP_1:14 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "C")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set (Var "D"))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "D")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ))) ; 
 
theorem :: TBSP_1:15 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "t1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "t1")) ($#k6_domain_1 :::"}"::: ) ))) "holds"  (Bool (Set (Var "P")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )))) ; 
 
theorem :: TBSP_1:16 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "P")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "P")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster   ($#v1_finset_1 :::"finite"::: )    ->   ($#v6_tbsp_1 :::"bounded"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 
end; registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 
end; 
theorem :: TBSP_1:17 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool  "("   "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "P")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )  ")" )) "holds"  (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "Y"))) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ))) ; 
 
theorem :: TBSP_1:18 (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "N")) "is"   ($#v5_tbsp_1 :::"bounded"::: )  ) "iff" (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "N"))) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )  ")" )) ; 
 registrationlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_tbsp_1 :::"bounded"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; 
cluster (Set   ($#k2_struct_0 :::"[#]"::: )  "N") ->   ($#v6_tbsp_1 :::"bounded"::: )   ; 
end; 
theorem :: TBSP_1:19 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    "st" (Bool (Bool (Set (Var "T")) "is"   ($#v1_tbsp_1 :::"totally_bounded"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v5_tbsp_1 :::"bounded"::: )  )) ; 
 definitionlet "N" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )  ; let "C" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "N")); assume 
(Bool (Set (Const "C")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )
 ; func  :::"diameter"::: "C" ->   ($#m1_subset_1 :::"Real":::) means :: TBSP_1:def 8 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "N"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "C") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "C")) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  it)  ")" ) & (Bool  "("   "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "N"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "C") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "C")) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )) "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )  ")" ) if (Bool "C"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 







:: deftheorem    defines :::"diameter"::: TBSP_1:def 8 :  (Bool  "for" (Set (Var "N")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "C")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b3")))  ")" ) & (Bool  "("   "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k2_metric_1 :::"dist"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )) "holds"  (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s")))  ")" )  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "C")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" )))); 
 
theorem :: TBSP_1:20 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: TBSP_1:21 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "S")))))) ; 
 
theorem :: TBSP_1:22 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ))))) ; 
 
theorem :: TBSP_1:23 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "t1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set  "("  ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "t1")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "r"))))))) ; 
 
theorem :: TBSP_1:24 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S")) "," (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "S")))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "V")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "S")))))) ; 
 
theorem :: TBSP_1:25 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "P")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set (Var "Q")) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ) & (Bool (Set (Var "P"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Q")))) "holds"  (Bool (Set   ($#k3_tbsp_1 :::"diameter"::: )  (Set  "(" (Set (Var "P"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Q")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "P")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k3_tbsp_1 :::"diameter"::: )  (Set (Var "Q")) ")" ))))) ; 
 
theorem :: TBSP_1:26 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_metric_1 :::"Reflexive"::: )     ($#v8_metric_1 :::"symmetric"::: )     ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "S1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v3_tbsp_1 :::"Cauchy"::: )  )) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "S1"))) "is"   ($#v6_tbsp_1 :::"bounded"::: )  ))) ;