:: FIN_TOPO semantic presentation begin theorem :: FIN_TOPO:1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))))))) ; theorem :: FIN_TOPO:2 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "A"))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))))))) ; scheme :: FIN_TOPO:sch 1 MaxFinSeqEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F4( ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" )) -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set F1 "(" ")" )) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) & (Bool (Set F4 "(" (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r2_xboole_0 :::"c<"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")))) ")" ) ")" ) ")" )) provided (Bool (Set F2 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool (Set F3 "(" ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) and (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set F4 "(" (Set (Var "A")) ")" )) & (Bool (Set F4 "(" (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) ")" )) proof end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; definitionlet "FT" be ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); func :::"U_FT"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 1 (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "FT") "," "x" ")" ); end; :: deftheorem defines :::"U_FT"::: FIN_TOPO:def 1 : (Bool "for" (Set (Var "FT")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "holds" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "FT"))) "," (Set (Var "x")) ")" )))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "y" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Const "x")) ($#k1_tarski :::"}"::: ) ); :: original: :::".-->"::: redefine func "x" :::".-->"::: "y" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ); end; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"SinglRel"::: "x" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) equals :: FIN_TOPO:def 2 (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) "x" "," "x" ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ); end; :: deftheorem defines :::"SinglRel"::: FIN_TOPO:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_fin_topo :::"SinglRel"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))); definitionfunc :::"FT{0}"::: -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) equals :: FIN_TOPO:def 3 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) "," (Set "(" ($#k3_fin_topo :::"SinglRel"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "#)" ); end; :: deftheorem defines :::"FT{0}"::: FIN_TOPO:def 3 : (Bool (Set ($#k4_fin_topo :::"FT{0}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) "," (Set "(" ($#k3_fin_topo :::"SinglRel"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "#)" )); registration cluster (Set ($#k4_fin_topo :::"FT{0}"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ; end; notationlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; synonym :::"filled"::: "IT" for :::"reflexive"::: ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "IT" is :::"reflexive"::: means :: FIN_TOPO:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"filled"::: FIN_TOPO:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_orders_2 :::"filled"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))))) ")" )); theorem :: FIN_TOPO:3 (Bool (Set ($#k4_fin_topo :::"FT{0}"::: ) ) "is" ($#v3_orders_2 :::"filled"::: ) ) ; registration cluster (Set ($#k4_fin_topo :::"FT{0}"::: ) ) -> ($#v8_struct_0 :::"finite"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"filled"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_orders_2 :::"strict"::: ) ($#v3_orders_2 :::"filled"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; theorem :: FIN_TOPO:4 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"filled"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "{" (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) : (Bool verum) "}" "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "FT")))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func "A" :::"^delta"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 5 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "FT" : (Bool "(" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) "A") & (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set "A" ($#k3_subset_1 :::"`"::: ) )) ")" ) "}" ; end; :: deftheorem defines :::"^delta"::: FIN_TOPO:def 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")) "holds" (Bool (Set (Set (Var "A")) ($#k5_fin_topo :::"^delta"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) : (Bool "(" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) & (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) ")" ) "}" ))); theorem :: FIN_TOPO:5 (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 "(" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) & (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) )) ")" ) ")" )))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func "A" :::"^deltai"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 6 (Set "A" ($#k9_subset_1 :::"/\"::: ) (Set "(" "A" ($#k5_fin_topo :::"^delta"::: ) ")" )); func "A" :::"^deltao"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 7 (Set (Set "(" "A" ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" "A" ($#k5_fin_topo :::"^delta"::: ) ")" )); end; :: deftheorem defines :::"^deltai"::: FIN_TOPO:def 6 : (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")) ($#k6_fin_topo :::"^deltai"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k5_fin_topo :::"^delta"::: ) ")" ))))); :: deftheorem defines :::"^deltao"::: FIN_TOPO:def 7 : (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")) ($#k7_fin_topo :::"^deltao"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k5_fin_topo :::"^delta"::: ) ")" ))))); theorem :: FIN_TOPO:6 (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")) ($#k6_fin_topo :::"^deltai"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k7_fin_topo :::"^deltao"::: ) ")" ))))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func "A" :::"^i"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 8 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "FT" : (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) "A") "}" ; func "A" :::"^b"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 9 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "FT" : (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) "A") "}" ; func "A" :::"^s"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 10 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "FT" : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"misses"::: ) "A") ")" ) "}" ; end; :: deftheorem defines :::"^i"::: FIN_TOPO:def 8 : (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")) ($#k8_fin_topo :::"^i"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) : (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "}" ))); :: deftheorem defines :::"^b"::: FIN_TOPO:def 9 : (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")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) : (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) "}" ))); :: deftheorem defines :::"^s"::: FIN_TOPO:def 10 : (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")) ($#k10_fin_topo :::"^s"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) : (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A"))) ")" ) "}" ))); definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func "A" :::"^n"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 11 (Set "A" ($#k7_subset_1 :::"\"::: ) (Set "(" "A" ($#k10_fin_topo :::"^s"::: ) ")" )); func "A" :::"^f"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 12 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "FT" : (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "FT" "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) "}" ; end; :: deftheorem defines :::"^n"::: FIN_TOPO:def 11 : (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")) ($#k11_fin_topo :::"^n"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k10_fin_topo :::"^s"::: ) ")" ))))); :: deftheorem defines :::"^f"::: FIN_TOPO:def 12 : (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")) ($#k12_fin_topo :::"^f"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) : (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) "}" ))); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "IT" is :::"symmetric"::: means :: FIN_TOPO:def 13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"symmetric"::: FIN_TOPO:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y"))))) ")" )); theorem :: FIN_TOPO:7 (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 (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" )))) ; theorem :: FIN_TOPO: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")) ($#k9_fin_topo :::"^b"::: ) )) "iff" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) ")" )))) ; theorem :: FIN_TOPO:9 (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 (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A"))) ")" ) ")" )))) ; theorem :: FIN_TOPO: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")) ($#k11_fin_topo :::"^n"::: ) )) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A"))) ")" ) ")" )))) ; theorem :: FIN_TOPO: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")) ($#k12_fin_topo :::"^f"::: ) )) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) ")" )) ")" )))) ; theorem :: FIN_TOPO:12 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool (Set (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k12_fin_topo :::"^f"::: ) ))) ")" )) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); attr "IT" is :::"open"::: means :: FIN_TOPO:def 14 (Bool "IT" ($#r1_hidden :::"="::: ) (Set "IT" ($#k8_fin_topo :::"^i"::: ) )); attr "IT" is :::"closed"::: means :: FIN_TOPO:def 15 (Bool "IT" ($#r1_hidden :::"="::: ) (Set "IT" ($#k9_fin_topo :::"^b"::: ) )); attr "IT" is :::"connected"::: means :: FIN_TOPO:def 16 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" "FT" "st" (Bool (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C")))); end; :: deftheorem defines :::"open"::: FIN_TOPO:def 14 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_fin_topo :::"open"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k8_fin_topo :::"^i"::: ) )) ")" ))); :: deftheorem defines :::"closed"::: FIN_TOPO:def 15 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_fin_topo :::"closed"::: ) ) "iff" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "IT")) ($#k9_fin_topo :::"^b"::: ) )) ")" ))); :: deftheorem defines :::"connected"::: FIN_TOPO:def 16 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_fin_topo :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C")))) ")" ))); definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); func "A" :::"^fb"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 17 (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" "FT" : (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "F")) "is" ($#v3_fin_topo :::"closed"::: ) ) ")" ) "}" ); func "A" :::"^fi"::: -> ($#m1_subset_1 :::"Subset":::) "of" "FT" equals :: FIN_TOPO:def 18 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" "FT" : (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "F")) "is" ($#v2_fin_topo :::"open"::: ) ) ")" ) "}" ); end; :: deftheorem defines :::"^fb"::: FIN_TOPO:def 17 : (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")) ($#k13_fin_topo :::"^fb"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) : (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "F")) "is" ($#v3_fin_topo :::"closed"::: ) ) ")" ) "}" )))); :: deftheorem defines :::"^fi"::: FIN_TOPO:def 18 : (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")) ($#k14_fin_topo :::"^fi"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "F")) where F "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) : (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "F")) "is" ($#v2_fin_topo :::"open"::: ) ) ")" ) "}" )))); theorem :: FIN_TOPO:13 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"filled"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) )))) ; theorem :: FIN_TOPO:14 (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")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) )))) ; theorem :: FIN_TOPO:15 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v3_orders_2 :::"filled"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "S")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "FT")))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")))) ")" ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "S")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")) ")" ))) ")" ))) ")" ))) ; theorem :: FIN_TOPO:16 (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 "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k8_fin_topo :::"^i"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) )))) ; theorem :: FIN_TOPO:17 (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 "(" (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_fin_topo :::"^i"::: ) )))) ; theorem :: FIN_TOPO:18 (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")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k9_fin_topo :::"^b"::: ) ")" ))))) ; theorem :: FIN_TOPO:19 (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 "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ($#k5_fin_topo :::"^delta"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_fin_topo :::"^delta"::: ) )))) ; theorem :: FIN_TOPO:20 (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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k10_fin_topo :::"^s"::: ) ))) "holds" (Bool "not" (Bool (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_fin_topo :::"^b"::: ) )))))) ; theorem :: FIN_TOPO:21 (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")) ($#k10_fin_topo :::"^s"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) )))) ; theorem :: FIN_TOPO:22 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"filled"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool (Set (Set (Var "A")) ($#k8_fin_topo :::"^i"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; theorem :: FIN_TOPO:23 (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 (Var "A")) "is" ($#v2_fin_topo :::"open"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_fin_topo :::"closed"::: ) ))) ; theorem :: FIN_TOPO:24 (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 (Var "A")) "is" ($#v3_fin_topo :::"closed"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_fin_topo :::"open"::: ) ))) ;