:: FINTOPO5 semantic presentation begin theorem :: FINTOPO5:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: FINTOPO5:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; definitionlet "FT1", "FT2" be ($#l1_orders_2 :::"RelStr"::: ) ; let "h" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "FT1")) "," (Set (Const "FT2")); attr "h" is :::"being_homeomorphism"::: means :: FINTOPO5:def 1 (Bool "(" (Bool "h" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "h" "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "FT1" "holds" (Bool (Set "h" ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "FT2") "," (Set "(" "h" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_homeomorphism"::: FINTOPO5:def 1 : (Bool "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2")) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) ) "iff" (Bool "(" (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "h")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT1")) "holds" (Bool (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "FT2"))) "," (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" ) ")" ) ")" ))); theorem :: FINTOPO5:3 (Bool "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT2")) "," (Set (Var "FT1")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k2_funct_1 :::"""::: ) )) & (Bool (Set (Var "g")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) ) ")" )))) ; theorem :: FINTOPO5:4 (Bool "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT2")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT1")) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) "iff" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "y")) "," (Set (Var "n")) ")" )) ")" ))))))) ; theorem :: FINTOPO5:5 (Bool "for" (Set (Var "FT1")) "," (Set (Var "FT2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "FT1")) "," (Set (Var "FT2")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT2")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT2")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" )) "iff" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "y")) "," (Set (Var "n")) ")" )) ")" ))))))) ; theorem :: FINTOPO5:6 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fintopo4 :::"is_continuous"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ))))) ; theorem :: FINTOPO5:7 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) ; theorem :: FINTOPO5:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "T")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ))))) ; theorem :: FINTOPO5:9 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "jn")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "jn")))) "holds" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set (Var "jn")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" )))) ; theorem :: FINTOPO5:10 (Bool "for" (Set (Var "kc")) "," (Set (Var "km")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fintopo4 :::"is_continuous"::: ) (Set (Var "kc"))) & (Bool (Set (Var "km")) ($#r1_hidden :::"="::: ) (Set ($#k2_int_1 :::"[/"::: ) (Set "(" (Set (Var "kc")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k2_int_1 :::"\]"::: ) ))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_fintopo3 :::"U_FT"::: ) "(" (Set (Var "p")) "," (Set (Var "km")) ")" )))))) ; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"Im"::: redefine func :::"Im"::: "(" "R" "," "x" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "B"; end; definitionlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Nbdl2"::: "(" "n" "," "m" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) means :: FINTOPO5:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ($#k2_zfmisc_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 "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_fintopo5 :::"Im"::: ) "(" it "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) "n" ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) "m" ")" ) "," (Set (Var "j")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))); end; :: deftheorem defines :::"Nbdl2"::: FINTOPO5:def 2 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_fintopo5 :::"Nbdl2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_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 "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_fintopo5 :::"Im"::: ) "(" (Set (Var "b3")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) (Set (Var "n")) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) (Set (Var "m")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ")" ))); definitionlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"FTSL2"::: "(" "n" "," "m" ")" -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) equals :: FINTOPO5:def 3 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k2_fintopo5 :::"Nbdl2"::: ) "(" "n" "," "m" ")" ")" ) "#)" ); end; :: deftheorem defines :::"FTSL2"::: FINTOPO5:def 3 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fintopo5 :::"FTSL2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k2_fintopo5 :::"Nbdl2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) "#)" ))); registrationlet "n", "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k3_fintopo5 :::"FTSL2"::: ) "(" "n" "," "m" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ; end; theorem :: FINTOPO5:11 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fintopo5 :::"FTSL2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) "is" ($#v3_orders_2 :::"filled"::: ) )) ; theorem :: FINTOPO5:12 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_fintopo5 :::"FTSL2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) "is" ($#v1_fin_topo :::"symmetric"::: ) )) ; theorem :: FINTOPO5:13 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k3_fintopo5 :::"FTSL2"::: ) "(" (Set (Var "n")) "," (Num 1) ")" ")" ) "," (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Var "h")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) ))) ; definitionlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Nbds2"::: "(" "n" "," "m" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) means :: FINTOPO5:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ($#k2_zfmisc_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 "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_fintopo5 :::"Im"::: ) "(" it "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) "m" ")" ) "," (Set (Var "j")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) "n" ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "j")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))))); end; :: deftheorem defines :::"Nbds2"::: FINTOPO5:def 4 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_fintopo5 :::"Nbds2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_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 "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k1_fintopo5 :::"Im"::: ) "(" (Set (Var "b3")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) (Set (Var "m")) ")" ) "," (Set (Var "j")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_fintopo5 :::"Im"::: ) "(" (Set "(" ($#k1_fintopo4 :::"Nbdl1"::: ) (Set (Var "n")) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "j")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))))) ")" ))); definitionlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"FTSS2"::: "(" "n" "," "m" ")" -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) equals :: FINTOPO5:def 5 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "m" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_fintopo5 :::"Nbds2"::: ) "(" "n" "," "m" ")" ")" ) "#)" ); end; :: deftheorem defines :::"FTSS2"::: FINTOPO5:def 5 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo5 :::"FTSS2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_fintopo5 :::"Nbds2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) "#)" ))); registrationlet "n", "m" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k5_fintopo5 :::"FTSS2"::: ) "(" "n" "," "m" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ; end; theorem :: FINTOPO5:14 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo5 :::"FTSS2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) "is" ($#v3_orders_2 :::"filled"::: ) )) ; theorem :: FINTOPO5:15 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_fintopo5 :::"FTSS2"::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ) "is" ($#v1_fin_topo :::"symmetric"::: ) )) ; theorem :: FINTOPO5:16 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_fintopo5 :::"FTSS2"::: ) "(" (Set (Var "n")) "," (Num 1) ")" ")" ) "," (Set "(" ($#k2_fintopo4 :::"FTSL1"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Var "h")) "is" ($#v1_fintopo5 :::"being_homeomorphism"::: ) ))) ;