:: FINTOPO4  semantic presentation begin  definitionlet "FT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "A", "B" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); pred "A" "," "B" :::"are_separated":::  means :: FINTOPO4:def 1 (Bool  "("  (Bool (Set "A"  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  "B") & (Bool "A"  ($#r1_xboole_0 :::"misses"::: )  (Set "B"  ($#k9_fin_topo :::"^b"::: )  ))  ")" ); symmetry  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT"))  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "A"))) & (Bool (Set (Var "B"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  ))  ")" ))
 ; end; 






:: deftheorem    defines :::"are_separated"::: FINTOPO4:def 1 :  (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  ) "iff" (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  ))  ")" )  ")" ))); 
 
theorem :: FINTOPO4:1 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k7_fintopo3 :::"Finf"::: )   "(" (Set (Var "A")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k7_fintopo3 :::"Finf"::: )   "(" (Set (Var "A")) "," (Set (Var "m")) ")" ))))) ; 
 
theorem :: FINTOPO4:2 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k3_fintopo3 :::"Fcl"::: )   "(" (Set (Var "A")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_fintopo3 :::"Fcl"::: )   "(" (Set (Var "A")) "," (Set (Var "m")) ")" ))))) ; 
 
theorem :: FINTOPO4:3 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k9_fintopo3 :::"Fdfl"::: )   "(" (Set (Var "A")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k9_fintopo3 :::"Fdfl"::: )   "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FINTOPO4:4 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k5_fintopo3 :::"Fint"::: )   "(" (Set (Var "A")) "," (Set (Var "m")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k5_fintopo3 :::"Fint"::: )   "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FINTOPO4:5 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  )) "holds"  (Bool (Set (Var "B")) "," (Set (Var "A"))  ($#r1_fintopo4 :::"are_separated"::: )  ))) ; 
 
theorem :: FINTOPO4:6 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  )) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))))) ; 
 
theorem :: FINTOPO4:7 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  ) "iff" (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k12_fin_topo :::"^f"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k12_fin_topo :::"^f"::: )  ))  ")" )  ")" ))) ; 
 
theorem :: FINTOPO4:8 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  ) & (Bool (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  )))) ; 
 
theorem :: FINTOPO4:9 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  ) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))))) ; 
 
theorem :: FINTOPO4:10 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  ) "iff" (Bool (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))  ")" ))) ; 
 
theorem :: FINTOPO4:11 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  ) "iff" (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  ))  ")" ))) ; 
 
theorem :: FINTOPO4:12 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_fin_topo :::"connected"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_fintopo4 :::"are_separated"::: )  ) & (Bool (Bool  "not" (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "IT"))))) "holds"  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "IT"))))  ")" ))) ; 
 
theorem :: FINTOPO4:13 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set (Var "FT")) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v4_fin_topo :::"connected"::: )  ) "iff" (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or"  "not" (Bool (Set (Set (Var "B"))  ($#k7_subset_1 :::"\"::: )  (Set (Var "C")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or"  "not" (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) "or"  "not" (Bool (Set (Set (Var "C"))  ($#k9_fin_topo :::"^b"::: )  )  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "B"))  ($#k7_subset_1 :::"\"::: )  (Set (Var "C"))))  ")" ))  ")" ))) ; 
 definitionlet "FT1", "FT2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "FT1")) "," (Set (Const "FT2")); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); pred "f" :::"is_continuous"::: "n" means :: FINTOPO4:def 2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "FT1"  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" "FT2"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "FT1")) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))) "holds"  (Bool (Set "f"  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k10_fintopo3 :::"U_FT"::: )   "(" (Set (Var "x")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_fintopo3 :::"U_FT"::: )   "(" (Set (Var "y")) "," "n" ")" )))); end; 







:: deftheorem    defines :::"is_continuous"::: FINTOPO4:def 2 :  (Bool  "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2"))  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set (Var "n"))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT1"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT2"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "FT1")))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k10_fintopo3 :::"U_FT"::: )   "(" (Set (Var "x")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_fintopo3 :::"U_FT"::: )   "(" (Set (Var "y")) "," (Set (Var "n")) ")" ))))  ")" )))); 
 
theorem :: FINTOPO4:14 (Bool  "for" (Set (Var "FT1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "FT2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set (Var "n"))))))) ; 
 
theorem :: FINTOPO4:15 (Bool  "for" (Set (Var "FT1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "FT2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"filled"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "n0")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set (Var "n0"))) & (Bool (Set (Var "n0"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set (Var "n"))))))) ; 
 
theorem :: FINTOPO4:16 (Bool  "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT1"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT2"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "(" (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k9_fin_topo :::"^b"::: )  )))))) ; 
 
theorem :: FINTOPO4:17 (Bool  "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT1"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT2"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_fin_topo :::"connected"::: )  ) & (Bool (Set (Var "f"))  ($#r2_fintopo4 :::"is_continuous"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "B")) "is"   ($#v4_fin_topo :::"connected"::: )  ))))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Nbdl1"::: "n" ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  "n" ")" ) means :: FINTOPO4:def 3 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  "n"))) "holds"  (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set  "("  ($#k7_nat_1 :::"max"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," "n" ")"  ")" ) ($#k1_enumset1 :::"}"::: ) ))); end; 





:: deftheorem    defines :::"Nbdl1"::: FINTOPO4:def 3 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_fintopo4 :::"Nbdl1"::: )  (Set (Var "n")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "b2")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set  "("  ($#k7_nat_1 :::"max"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Num 1) ")"  ")" ) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "n")) ")"  ")" ) ($#k1_enumset1 :::"}"::: ) )))  ")" ))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func  :::"FTSL1"::: "n" ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   equals :: FINTOPO4:def 4 (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  "n" ")" ) "," (Set  "("  ($#k1_fintopo4 :::"Nbdl1"::: )  "n" ")" ) "#)" ); end; 






:: deftheorem    defines :::"FTSL1"::: FINTOPO4:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_fintopo4 :::"FTSL1"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k1_fintopo4 :::"Nbdl1"::: )  (Set (Var "n")) ")" ) "#)" ))); 
 
theorem :: FINTOPO4:18 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_fintopo4 :::"FTSL1"::: )  (Set (Var "n"))) "is"   ($#v3_orders_2 :::"filled"::: )  )) ; 
 
theorem :: FINTOPO4:19 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_fintopo4 :::"FTSL1"::: )  (Set (Var "n"))) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Nbdc1"::: "n" ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  "n" ")" ) means :: FINTOPO4:def 5 (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  "n"))) "holds"  (Bool  "("   "("  (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  "n")) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k1_enumset1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  "n")) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," "n" "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k1_enumset1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  "n")) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Num 1) ($#k1_enumset1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  "n")) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" it "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ))  ")"   ")" )); end; 





:: deftheorem    defines :::"Nbdc1"::: FINTOPO4:def 5 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_fintopo4 :::"Nbdc1"::: )  (Set (Var "n")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "b2")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k1_enumset1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "b2")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set (Var "n")) "," (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ($#k1_enumset1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "b2")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "i")) "," (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) "," (Num 1) ($#k1_enumset1 :::"}"::: ) ))  ")"  &  "("  (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "implies" (Bool (Set   ($#k9_relat_1 :::"Im"::: )   "(" (Set (Var "b2")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ))  ")"   ")" ))  ")" ))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))
 ; func  :::"FTSC1"::: "n" ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   equals :: FINTOPO4:def 6 (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  "n" ")" ) "," (Set  "("  ($#k3_fintopo4 :::"Nbdc1"::: )  "n" ")" ) "#)" ); end; 






:: deftheorem    defines :::"FTSC1"::: FINTOPO4:def 6 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_fintopo4 :::"FTSC1"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k3_fintopo4 :::"Nbdc1"::: )  (Set (Var "n")) ")" ) "#)" ))); 
 
theorem :: FINTOPO4:20 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_fintopo4 :::"FTSC1"::: )  (Set (Var "n"))) "is"   ($#v3_orders_2 :::"filled"::: )  )) ; 
 
theorem :: FINTOPO4:21 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_fintopo4 :::"FTSC1"::: )  (Set (Var "n"))) "is"   ($#v1_fin_topo :::"symmetric"::: )  )) ;