:: FINTOPO3 semantic presentation begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "A" :::"^d"::: -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: FINTOPO3:def 1 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "T" : (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "A" ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))))) "}" ; end; :: deftheorem defines :::"^d"::: FINTOPO3:def 1 : (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) : (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))))) "}" ))); theorem :: FINTOPO3:1 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k12_fin_topo :::"^f"::: ) )))) ; theorem :: FINTOPO3:2 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) )) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))))) ")" )))) ; theorem :: FINTOPO3:3 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; theorem :: FINTOPO3:4 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k12_fin_topo :::"^f"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: FINTOPO3:5 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k12_fin_topo :::"^f"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k12_fin_topo :::"^f"::: ) )))) ; theorem :: FINTOPO3:6 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_fintopo3 :::"^d"::: ) )))) ; theorem :: FINTOPO3:7 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ")" ))))) ; theorem :: FINTOPO3:8 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ")" ))))) ; theorem :: FINTOPO3:9 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_fin_topo :::"^i"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k8_fin_topo :::"^i"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k8_fin_topo :::"^i"::: ) )))) ; theorem :: FINTOPO3:10 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_fin_topo :::"^i"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k8_fin_topo :::"^i"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k8_fin_topo :::"^i"::: ) )))) ; theorem :: FINTOPO3:11 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k12_fin_topo :::"^f"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k12_fin_topo :::"^f"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k12_fin_topo :::"^f"::: ) )))) ; theorem :: FINTOPO3:12 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k1_fintopo3 :::"^d"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k1_fintopo3 :::"^d"::: ) )))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Fcl"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: FINTOPO3:def 2 (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ))) ")" ) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "A") ")" ); end; :: deftheorem defines :::"Fcl"::: FINTOPO3:def 2 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_fintopo3 :::"Fcl"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ))) ")" ) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ) ")" )))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "n" be ($#m1_hidden :::"Nat":::); func :::"Fcl"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: FINTOPO3:def 3 (Set (Set "(" ($#k2_fintopo3 :::"Fcl"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Fcl"::: FINTOPO3:def 3 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fintopo3 :::"Fcl"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Fint"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: FINTOPO3:def 4 (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k8_fin_topo :::"^i"::: ) ))) ")" ) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "A") ")" ); end; :: deftheorem defines :::"Fint"::: FINTOPO3:def 4 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_fintopo3 :::"Fint"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k8_fin_topo :::"^i"::: ) ))) ")" ) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ) ")" )))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "n" be ($#m1_hidden :::"Nat":::); func :::"Fint"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: FINTOPO3:def 5 (Set (Set "(" ($#k4_fintopo3 :::"Fint"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Fint"::: FINTOPO3:def 5 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_fintopo3 :::"Fint"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))); theorem :: FINTOPO3:13 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k9_fin_topo :::"^b"::: ) ))))) ; theorem :: FINTOPO3:14 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FINTOPO3:15 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) )))) ; theorem :: FINTOPO3:16 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k9_fin_topo :::"^b"::: ) )))) ; theorem :: FINTOPO3:17 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: FINTOPO3:18 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k8_fin_topo :::"^i"::: ) ))))) ; theorem :: FINTOPO3:19 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FINTOPO3:20 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_fin_topo :::"^i"::: ) )))) ; theorem :: FINTOPO3:21 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_fin_topo :::"^i"::: ) ")" ) ($#k8_fin_topo :::"^i"::: ) )))) ; theorem :: FINTOPO3:22 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: FINTOPO3:23 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: FINTOPO3:24 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: FINTOPO3:25 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: FINTOPO3:26 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: FINTOPO3:27 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: FINTOPO3:28 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: FINTOPO3:29 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: FINTOPO3:30 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k5_fintopo3 :::"Fint"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_fintopo3 :::"Fcl"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Finf"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: FINTOPO3:def 6 (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k12_fin_topo :::"^f"::: ) ))) ")" ) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "A") ")" ); end; :: deftheorem defines :::"Finf"::: FINTOPO3:def 6 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_fintopo3 :::"Finf"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k12_fin_topo :::"^f"::: ) ))) ")" ) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ) ")" )))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "n" be ($#m1_hidden :::"Nat":::); func :::"Finf"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: FINTOPO3:def 7 (Set (Set "(" ($#k6_fintopo3 :::"Finf"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Finf"::: FINTOPO3:def 7 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_fintopo3 :::"Finf"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Fdfl"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" ) means :: FINTOPO3:def 8 (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_fintopo3 :::"^d"::: ) ))) ")" ) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "A") ")" ); end; :: deftheorem defines :::"Fdfl"::: FINTOPO3:def 8 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_fintopo3 :::"Fdfl"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k1_fintopo3 :::"^d"::: ) ))) ")" ) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ) ")" )))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); let "n" be ($#m1_hidden :::"Nat":::); func :::"Fdfl"::: "(" "A" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: FINTOPO3:def 9 (Set (Set "(" ($#k8_fintopo3 :::"Fdfl"::: ) "A" ")" ) ($#k1_funct_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Fdfl"::: FINTOPO3:def 9 : (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_fintopo3 :::"Fdfl"::: ) (Set (Var "A")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))); theorem :: FINTOPO3:31 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k12_fin_topo :::"^f"::: ) ))))) ; theorem :: FINTOPO3:32 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FINTOPO3:33 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k12_fin_topo :::"^f"::: ) )))) ; theorem :: FINTOPO3:34 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k12_fin_topo :::"^f"::: ) ")" ) ($#k12_fin_topo :::"^f"::: ) )))) ; theorem :: FINTOPO3:35 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: FINTOPO3:36 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: FINTOPO3:37 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: FINTOPO3:38 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k1_fintopo3 :::"^d"::: ) ))))) ; theorem :: FINTOPO3:39 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FINTOPO3:40 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) )))) ; theorem :: FINTOPO3:41 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Num 2) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_fintopo3 :::"^d"::: ) ")" ) ($#k1_fintopo3 :::"^d"::: ) )))) ; theorem :: FINTOPO3:42 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: FINTOPO3:43 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: FINTOPO3:44 (Bool "for" (Set (Var "T")) "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 "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ))))) ; theorem :: FINTOPO3:45 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_fintopo3 :::"Finf"::: ) "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: FINTOPO3:46 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "A")) "," (Set (Var "n")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k9_fintopo3 :::"Fdfl"::: ) "(" (Set (Var "B")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_fintopo3 :::"Finf"::: ) "(" (Set "(" (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k3_subset_1 :::"`"::: ) ")" ) "," (Set (Var "n")) ")" ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "T")); func :::"U_FT"::: "(" "x" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: FINTOPO3:def 10 (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set "(" ($#k1_fin_topo :::"U_FT"::: ) "x" ")" ) "," "n" ")" ); end; :: deftheorem defines :::"U_FT"::: FINTOPO3:def 10 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" ) "," (Set (Var "n")) ")" ))))); theorem :: FINTOPO3:47 (Bool "for" (Set (Var "T")) "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 "T")) "holds" (Bool (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")))))) ; theorem :: FINTOPO3:48 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ")" ) ($#k12_fin_topo :::"^f"::: ) ))))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; pred "S" "," "T" :::"are_mutually_symmetric"::: means :: FINTOPO3:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ); symmetry (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) ")" ) ")" )) ; end; :: deftheorem defines :::"are_mutually_symmetric"::: FINTOPO3:def 11 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r1_fintopo3 :::"are_mutually_symmetric"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ) ")" ));