:: FINTOPO2  semantic presentation begin  






theorem :: FINTOPO2: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"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fin_topo :::"^i"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k8_fin_topo :::"^i"::: )  )))) ; 
 
theorem :: FINTOPO2:2 (Bool  "for" (Set (Var "FT")) "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 "FT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k5_fin_topo :::"^delta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k8_fin_topo :::"^i"::: )  ")" )  ($#k3_subset_1 :::"`"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:3 (Bool  "for" (Set (Var "FT")) "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 "FT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k5_fin_topo :::"^delta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "(" (Set (Var "A"))  ($#k8_fin_topo :::"^i"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:4 (Bool  "for" (Set (Var "FT")) "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 "FT"))  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v2_fin_topo :::"open"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v3_fin_topo :::"closed"::: )  ))) ; 
 
theorem :: FINTOPO2:5 (Bool  "for" (Set (Var "FT")) "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 "FT"))  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v3_fin_topo :::"closed"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v2_fin_topo :::"open"::: )  ))) ; 
 definitionlet "FT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func  :::"P_1":::  "(" "x" "," "y" "," "A" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: FINTOPO2:def 1 (Set   ($#k8_margrel1 :::"TRUE"::: )  ) if (Bool  "("  (Bool "y"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  "x")) & (Bool "y"  ($#r2_hidden :::"in"::: )  "A")  ")" )  otherwise (Set   ($#k7_margrel1 :::"FALSE"::: )  ); end; 








:: deftheorem    defines :::"P_1"::: FINTOPO2:def 1 :  (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "implies" (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )) "implies" (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")"   ")" )))); 
 definitionlet "FT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func  :::"P_2":::  "(" "x" "," "y" "," "A" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: FINTOPO2:def 2 (Set   ($#k8_margrel1 :::"TRUE"::: )  ) if (Bool  "("  (Bool "y"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  "x")) & (Bool "y"  ($#r2_hidden :::"in"::: )  (Set "A"  ($#k3_subset_1 :::"`"::: )  ))  ")" )  otherwise (Set   ($#k7_margrel1 :::"FALSE"::: )  ); end; 








:: deftheorem    defines :::"P_2"::: FINTOPO2:def 2 :  (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ))) "implies" (Bool (Set   ($#k2_fintopo2 :::"P_2"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ))  ")" )) "implies" (Bool (Set   ($#k2_fintopo2 :::"P_2"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")"   ")" )))); 
 
theorem :: FINTOPO2:6 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:7 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set   ($#k2_fintopo2 :::"P_2"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ))  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:8 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k5_fin_topo :::"^delta"::: )  )) "iff" (Bool  "ex" (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st"  (Bool  "("  (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set   ($#k2_fintopo2 :::"P_2"::: )   "(" (Set (Var "x")) "," (Set (Var "y2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" ))  ")" )))) ; 
 definitionlet "FT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); func  :::"P_0":::  "(" "x" "," "y" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: FINTOPO2:def 3 (Set   ($#k8_margrel1 :::"TRUE"::: )  ) if (Bool "y"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  "x"))  otherwise (Set   ($#k7_margrel1 :::"FALSE"::: )  ); end; 







:: deftheorem    defines :::"P_0"::: FINTOPO2:def 3 :  (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x"))))) "implies" (Bool (Set   ($#k3_fintopo2 :::"P_0"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x")))))) "implies" (Bool (Set   ($#k3_fintopo2 :::"P_0"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")"   ")" ))); 
 
theorem :: FINTOPO2:9 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set   ($#k3_fintopo2 :::"P_0"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_fin_topo :::"U_FT"::: )  (Set (Var "x"))))  ")" ))) ; 
 
theorem :: FINTOPO2:10 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k8_fin_topo :::"^i"::: )  )) "iff" (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  "st" (Bool (Bool (Set   ($#k3_fintopo2 :::"P_0"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))) "holds"  (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )))  ")" )))) ; 
 
theorem :: FINTOPO2:11 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k9_fin_topo :::"^b"::: )  )) "iff" (Bool  "ex" (Set (Var "y1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )))  ")" )))) ; 
 definitionlet "FT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func  :::"P_A":::  "(" "x" "," "A" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: FINTOPO2:def 4 (Set   ($#k8_margrel1 :::"TRUE"::: )  ) if (Bool "x"  ($#r2_hidden :::"in"::: )  "A")  otherwise (Set   ($#k7_margrel1 :::"FALSE"::: )  ); end; 







:: deftheorem    defines :::"P_A"::: FINTOPO2:def 4 :  (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "implies" (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))) "implies" (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")"   ")" )))); 
 
theorem :: FINTOPO2:12 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )))) ; 
 
theorem :: FINTOPO2:13 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_fin_topo :::"^deltai"::: )  )) "iff" (Bool  "("  (Bool  "ex" (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st"  (Bool  "("  (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set   ($#k2_fintopo2 :::"P_2"::: )   "(" (Set (Var "x")) "," (Set (Var "y2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" )) & (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:14 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k7_fin_topo :::"^deltao"::: )  )) "iff" (Bool  "("  (Bool  "ex" (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st"  (Bool  "("  (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set   ($#k2_fintopo2 :::"P_2"::: )   "(" (Set (Var "x")) "," (Set (Var "y2")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" )) & (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")" )  ")" )))) ; 
 definitionlet "FT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); func  :::"P_e":::  "(" "x" "," "y" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k6_margrel1 :::"BOOLEAN"::: )  ) equals :: FINTOPO2:def 5 (Set   ($#k8_margrel1 :::"TRUE"::: )  ) if (Bool "x"  ($#r1_hidden :::"="::: )  "y")  otherwise (Set   ($#k7_margrel1 :::"FALSE"::: )  ); end; 







:: deftheorem    defines :::"P_e"::: FINTOPO2:def 5 :  (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "implies" (Bool (Set   ($#k5_fintopo2 :::"P_e"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) "implies" (Bool (Set   ($#k5_fintopo2 :::"P_e"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")"   ")" ))); 
 
theorem :: FINTOPO2:15 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set   ($#k5_fintopo2 :::"P_e"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" ))) ; 
 
theorem :: FINTOPO2:16 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k10_fin_topo :::"^s"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  "holds"  (Bool  "("   "not" (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) "or"  "not" (Bool (Set   ($#k5_fintopo2 :::"P_e"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:17 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k11_fin_topo :::"^n"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "x")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st"  (Bool  "("  (Bool (Set   ($#k1_fintopo2 :::"P_1"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set   ($#k5_fintopo2 :::"P_e"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_margrel1 :::"FALSE"::: )  ))  ")" ))  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:18 (Bool  "for" (Set (Var "FT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k12_fin_topo :::"^f"::: )  )) "iff" (Bool  "ex" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st"  (Bool  "("  (Bool (Set   ($#k4_fintopo2 :::"P_A"::: )   "(" (Set (Var "y")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  )) & (Bool (Set   ($#k3_fintopo2 :::"P_0"::: )   "(" (Set (Var "y")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_margrel1 :::"TRUE"::: )  ))  ")" ))  ")" )))) ; 
 begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"FMT_Space_Str":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"FMT_Space_Str":::(# :::"carrier":::, :::"BNbd"::: #) ->    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; sel  :::"BNbd"::: "c1" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1") "," (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1") ")" ) ")" ); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_fintopo2 :::"strict"::: )    for    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; 
end; 









definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FMT")); func  :::"U_FMT"::: "x" ->   ($#m1_subset_1 :::"Subset-Family":::) "of" "FMT" equals :: FINTOPO2:def 6 (Set (Set  "the"  ($#u1_fintopo2 :::"BNbd"::: )  "of" "FMT")  ($#k3_funct_2 :::"."::: )  "x"); end; 






:: deftheorem    defines :::"U_FMT"::: FINTOPO2:def 6 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_fintopo2 :::"BNbd"::: )  "of" (Set (Var "FMT")))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))))); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"NeighSp"::: "T" ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_fintopo2 :::"strict"::: )     ($#l1_fintopo2 :::"FMT_Space_Str"::: )   means :: FINTOPO2:def 7 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" it "holds"  (Bool (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "V")) where V "is"   ($#m1_subset_1 :::"Subset":::) "of" "T" : (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "T")) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))  ")" )  "}"  )  ")" )  ")" ); end; 





:: deftheorem    defines :::"NeighSp"::: FINTOPO2:def 7 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "b2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_fintopo2 :::"strict"::: )     ($#l1_fintopo2 :::"FMT_Space_Str"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_fintopo2 :::"NeighSp"::: )  (Set (Var "T")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "b2")) "holds"  (Bool (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "V")) where V "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) : (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V")))  ")" )  "}"  )  ")" )  ")" )  ")" ))); 
 





definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; attr "IT" is  :::"Fo_filled":::  means :: FINTOPO2:def 8 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "IT"  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "IT"  "st" (Bool (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))))); end; 




:: deftheorem    defines :::"Fo_filled"::: FINTOPO2:def 8 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_fintopo2 :::"Fo_filled"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT"))  (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))))  ")" )); 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); func "A" :::"^Fodelta":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 9  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "FMT" : (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "FMT"  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "("  (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  "A") & (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set "A"  ($#k3_subset_1 :::"`"::: )  ))  ")" ))  "}"  ; end; 






:: deftheorem    defines :::"^Fodelta"::: FINTOPO2:def 9 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) : (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "("  (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A"))) & (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ))  ")" ))  "}"  ))); 
 
theorem :: FINTOPO2:19 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )) "iff" (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "("  (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A"))) & (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ))  ")" ))  ")" )))) ; 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); func "A" :::"^Fob":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 10  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "FMT" : (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "FMT"  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  "A"))  "}"  ; end; 






:: deftheorem    defines :::"^Fob"::: FINTOPO2:def 10 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) : (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A"))))  "}"  ))); 
 
theorem :: FINTOPO2:20 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  )) "iff" (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "W"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A"))))  ")" )))) ; 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); func "A" :::"^Foi":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 11  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "FMT" : (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "FMT" "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  "A")  ")" ))  "}"  ; end; 






:: deftheorem    defines :::"^Foi"::: FINTOPO2:def 11 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) : (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" ))  "}"  ))); 
 
theorem :: FINTOPO2:21 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  )) "iff" (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" ))  ")" )))) ; 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); func "A" :::"^Fos":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 12  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" "FMT" : (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "A") & (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "FMT" "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "V"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_xboole_0 :::"misses"::: )  "A")  ")" ))  ")" )  "}"  ; end; 






:: deftheorem    defines :::"^Fos"::: FINTOPO2:def 12 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_fintopo2 :::"^Fos"::: )  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) : (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "V"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "A")))  ")" ))  ")" )  "}"  ))); 
 
theorem :: FINTOPO2:22 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k11_fintopo2 :::"^Fos"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "V"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "A")))  ")" ))  ")" )  ")" )))) ; 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); func "A" :::"^Fon":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 13 (Set "A"  ($#k7_subset_1 :::"\"::: )  (Set  "(" "A"  ($#k11_fintopo2 :::"^Fos"::: )  ")" )); end; 






:: deftheorem    defines :::"^Fon"::: FINTOPO2:def 13 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k12_fintopo2 :::"^Fon"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set  "(" (Set (Var "A"))  ($#k11_fintopo2 :::"^Fos"::: )  ")" ))))); 
 
theorem :: FINTOPO2:23 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k12_fintopo2 :::"^Fon"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "V"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Set (Var "V"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:24 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k9_fintopo2 :::"^Fob"::: )  )))) ; 
 
theorem :: FINTOPO2:25 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k10_fintopo2 :::"^Foi"::: )  )))) ; 
 
theorem :: FINTOPO2:26 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k9_fintopo2 :::"^Fob"::: )  )))) ; 
 
theorem :: FINTOPO2:27 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k9_fintopo2 :::"^Fob"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "B"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:28 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k10_fintopo2 :::"^Foi"::: )  )))) ; 
 
theorem :: FINTOPO2:29 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k10_fintopo2 :::"^Foi"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "B"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:30 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )   "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "V1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "V2"))))  ")" )))  ")" ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k9_fintopo2 :::"^Fob"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" ))))  ")" )) ; 
 
theorem :: FINTOPO2:31 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )   "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "V1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "V2"))))  ")" )))  ")" ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "B"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k10_fintopo2 :::"^Foi"::: )  )))  ")" )) ; 
 
theorem :: FINTOPO2:32 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "V1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "V2"))))  ")" )))  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:33 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    "st" (Bool (Bool (Set (Var "FMT")) "is"   ($#v2_fintopo2 :::"Fo_filled"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "V1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "V2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "st"  (Bool  "("  (Bool (Set (Var "W"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x")))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "V1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "V2"))))  ")" ))))) ; 
 
theorem :: FINTOPO2:34 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k11_fintopo2 :::"^Fos"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )  ($#k9_fintopo2 :::"^Fob"::: )  )))  ")" )  ")" )))) ; 
 
theorem :: FINTOPO2:35 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )   "holds"   (Bool  "("  (Bool (Set (Var "FMT")) "is"   ($#v2_fintopo2 :::"Fo_filled"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  )))  ")" )) ; 
 
theorem :: FINTOPO2:36 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )   "holds"   (Bool  "("  (Bool (Set (Var "FMT")) "is"   ($#v2_fintopo2 :::"Fo_filled"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))  ")" )) ; 
 
theorem :: FINTOPO2:37 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  )))) ; 
 
theorem :: FINTOPO2:38 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k10_fintopo2 :::"^Foi"::: )  ")" )  ($#k3_subset_1 :::"`"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  )))) ; 
 
theorem :: FINTOPO2:39 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k9_fintopo2 :::"^Fob"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:40 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" )  ($#k3_subset_1 :::"`"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:41 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k8_fintopo2 :::"^Fodelta"::: )  )))) ; 
 
theorem :: FINTOPO2:42 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "(" (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" ))))) ; 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); func "A" :::"^Fodel_i":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 14 (Set "A"  ($#k9_subset_1 :::"/\"::: )  (Set  "(" "A"  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" )); func "A" :::"^Fodel_o":::  ->   ($#m1_subset_1 :::"Subset":::) "of" "FMT" equals :: FINTOPO2:def 15 (Set (Set  "(" "A"  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" "A"  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" )); end; 












:: deftheorem    defines :::"^Fodel_i"::: FINTOPO2:def 14 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k13_fintopo2 :::"^Fodel_i"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" ))))); 
 
:: deftheorem    defines :::"^Fodel_o"::: FINTOPO2:def 15 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k14_fintopo2 :::"^Fodel_o"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  ")" ))))); 
 
theorem :: FINTOPO2:43 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set (Set (Var "A"))  ($#k8_fintopo2 :::"^Fodelta"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k13_fintopo2 :::"^Fodel_i"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k14_fintopo2 :::"^Fodel_o"::: )  ")" ))))) ; 
 definitionlet "FMT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )  ; let "G" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FMT")); attr "G" is  :::"Fo_open":::  means :: FINTOPO2:def 16 (Bool "G"  ($#r1_hidden :::"="::: )  (Set "G"  ($#k10_fintopo2 :::"^Foi"::: )  )); attr "G" is  :::"Fo_closed":::  means :: FINTOPO2:def 17 (Bool "G"  ($#r1_hidden :::"="::: )  (Set "G"  ($#k9_fintopo2 :::"^Fob"::: )  )); end; 










:: deftheorem    defines :::"Fo_open"::: FINTOPO2:def 16 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v3_fintopo2 :::"Fo_open"::: )  ) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k10_fintopo2 :::"^Foi"::: )  ))  ")" ))); 
 
:: deftheorem    defines :::"Fo_closed"::: FINTOPO2:def 17 :  (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT")) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v4_fintopo2 :::"Fo_closed"::: )  ) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k9_fintopo2 :::"^Fob"::: )  ))  ")" ))); 
 
theorem :: FINTOPO2:44 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v3_fintopo2 :::"Fo_open"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_fintopo2 :::"Fo_closed"::: )  ))) ; 
 
theorem :: FINTOPO2:45 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v4_fintopo2 :::"Fo_closed"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v3_fintopo2 :::"Fo_open"::: )  ))) ; 
 
theorem :: FINTOPO2:46 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "FMT")) "is"   ($#v2_fintopo2 :::"Fo_filled"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k9_fintopo2 :::"^Fob"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "B"))  ($#k9_fintopo2 :::"^Fob"::: )  ")" ))))) ; 
 
theorem :: FINTOPO2:47 (Bool  "for" (Set (Var "FMT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_fintopo2 :::"FMT_Space_Str"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FMT"))  "st" (Bool (Bool (Set (Var "FMT")) "is"   ($#v2_fintopo2 :::"Fo_filled"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FMT")) "holds"  (Bool (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k6_fintopo2 :::"U_FMT"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k10_fintopo2 :::"^Foi"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k10_fintopo2 :::"^Foi"::: )  )))) ;