:: FINTOPO6 semantic presentation begin registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v4_fin_topo :::"connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "FT"))); end; theorem :: FINTOPO6:1 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool (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 :: FINTOPO6:2 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")) ")" ) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set (Set "(" ($#k1_struct_0 :::"{}"::: ) "FT" ")" ) ($#k9_fin_topo :::"^b"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: FINTOPO6:3 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool "(" "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) ($#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 "(" (Bool (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"meets"::: ) (Set (Set (Var "C")) ($#k9_fin_topo :::"^b"::: ) )) ")" ) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "FT" is :::"connected"::: means :: FINTOPO6:def 1 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "FT") "is" ($#v4_fin_topo :::"connected"::: ) ); end; :: deftheorem defines :::"connected"::: FINTOPO6:def 1 : (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_fintopo6 :::"connected"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT"))) "is" ($#v4_fin_topo :::"connected"::: ) ) ")" )); theorem :: FINTOPO6:4 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) )) "holds" (Bool "for" (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2")))) & (Bool (Set (Var "A2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2"))) & (Bool (Set (Var "A2")) "," (Set (Var "B2")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))))) "holds" (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT"))))))) ; theorem :: FINTOPO6:5 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))))) ; theorem :: FINTOPO6:6 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "B")) ($#k9_fin_topo :::"^b"::: ) )))) ; theorem :: FINTOPO6: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")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool "(" "for" (Set (Var "A2")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B2")))) & (Bool (Set (Var "A2")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B2"))) & (Bool (Set (Var "A2")) "," (Set (Var "B2")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))))) "holds" (Bool (Set (Var "B2")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; definitionlet "T" be ($#l1_orders_2 :::"RelStr"::: ) ; mode :::"SubSpace"::: "of" "T" -> ($#l1_orders_2 :::"RelStr"::: ) means :: FINTOPO6:def 2 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" it "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) "holds" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "T") "," (Set (Var "x")) ")" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" ) ")" ); end; :: deftheorem defines :::"SubSpace"::: FINTOPO6:def 2 : (Bool "for" (Set (Var "T")) "," (Set (Var "b2")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "T"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) "holds" (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_relat_1 :::"Im"::: ) "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "T"))) "," (Set (Var "x")) ")" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" ) ")" ) ")" )); registrationlet "T" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_orders_2 :::"strict"::: ) for ($#m1_fintopo6 :::"SubSpace"::: ) "of" "T"; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) for ($#m1_fintopo6 :::"SubSpace"::: ) "of" "T"; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func "T" :::"|"::: "P" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" "T" means :: FINTOPO6:def 3 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) "P"); end; :: deftheorem defines :::"|"::: FINTOPO6:def 3 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_fintopo6 :::"|"::: ) (Set (Var "P")))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "P"))) ")" )))); theorem :: FINTOPO6: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v3_orders_2 :::"filled"::: ) ))) ; registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"filled"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"filled"::: ) for ($#m1_fintopo6 :::"SubSpace"::: ) "of" "FT"; end; theorem :: FINTOPO6: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v1_fin_topo :::"symmetric"::: ) ))) ; theorem :: FINTOPO6:10 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X9")) "being" ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")))))) ; theorem :: FINTOPO6:11 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v3_fin_topo :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "P")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_fin_topo :::"open"::: ) ) ")" ))) ; theorem :: FINTOPO6: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 "(" (Bool (Set (Var "A")) "is" ($#v2_fin_topo :::"open"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "z"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) & (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 (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" ) ")" ))) ; theorem :: FINTOPO6:13 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A1")))) "holds" (Bool (Set (Set (Var "A1")) ($#k9_fin_topo :::"^b"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X9")) ")" ))))))) ; theorem :: FINTOPO6:14 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) (Bool "for" (Set (Var "P1")) "," (Set (Var "Q1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "P1"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "Q1"))) & (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r1_fintopo4 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "P1")) "," (Set (Var "Q1")) ($#r1_fintopo4 :::"are_separated"::: ) ))))) ; theorem :: FINTOPO6:15 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "P1")) "," (Set (Var "Q1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "st" (Bool (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set (Var "P1"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Var "Q1"))) & (Bool (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X9")))) & (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r1_fintopo4 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "P1")) "," (Set (Var "Q1")) ($#r1_fintopo4 :::"are_separated"::: ) ))))) ; theorem :: FINTOPO6: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" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) "iff" (Bool (Set (Set (Var "FT")) ($#k1_fintopo6 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_fintopo6 :::"connected"::: ) ) ")" ))) ; theorem :: FINTOPO6:17 (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" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Q")))) & (Bool (Set (Var "P")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Q"))) & (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Bool "not" (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))))) "holds" (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT"))))) ")" ))) ; theorem :: FINTOPO6: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")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k5_fin_topo :::"^delta"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FINTOPO6: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")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k6_fin_topo :::"^deltai"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FINTOPO6:20 (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 "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k7_fin_topo :::"^deltao"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FINTOPO6: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")) "holds" (Bool (Set (Set (Var "A")) ($#k6_fin_topo :::"^deltai"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "A")) ($#k7_fin_topo :::"^deltao"::: ) )))) ; theorem :: FINTOPO6: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")) ($#k7_fin_topo :::"^deltao"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_fin_topo :::"^b"::: ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))))) ; theorem :: FINTOPO6:23 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_fin_topo :::"^deltao"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))))) ; theorem :: FINTOPO6:24 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "A")) ($#k7_fin_topo :::"^deltao"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "B")) ($#k7_fin_topo :::"^deltao"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ))) ; theorem :: FINTOPO6:25 (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 :::"Point":::) "of" (Set (Var "FT")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "FT")); cluster (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) -> ($#v4_fin_topo :::"connected"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "FT"; end; 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")); pred "A" :::"is_a_component_of"::: "FT" means :: FINTOPO6:def 4 (Bool "(" (Bool "A" "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "FT" "st" (Bool (Bool (Set (Var "B")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool "A" ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" ); end; :: deftheorem defines :::"is_a_component_of"::: FINTOPO6:def 4 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" ) ")" ) ")" ))); theorem :: FINTOPO6:26 (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")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))))) ; theorem :: FINTOPO6:27 (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")) "is" ($#v3_fin_topo :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_fin_topo :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ))) ; theorem :: FINTOPO6:28 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_fin_topo :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v3_fin_topo :::"closed"::: ) ) ")" ))) ; theorem :: FINTOPO6:29 (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")) "," (Set (Var "A1")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "B1")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A1")) "," (Set (Var "B1")) ($#r1_fintopo4 :::"are_separated"::: ) ))) ; theorem :: FINTOPO6:30 (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")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Set (Var "A")) "," (Set (Var "C")) ($#r1_fintopo4 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C"))) ($#r1_fintopo4 :::"are_separated"::: ) ))) ; theorem :: FINTOPO6:31 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))) & (Bool (Set (Var "A")) "is" ($#v3_fin_topo :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_fin_topo :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) )) ; theorem :: FINTOPO6:32 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "FT")))) & (Bool (Set (Var "A")) "is" ($#v3_fin_topo :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_fin_topo :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B"))))) ; theorem :: FINTOPO6:33 (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")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "B")) "," (Set (Var "C")) ($#r1_fintopo4 :::"are_separated"::: ) ) & (Bool (Bool "not" (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))))) ; theorem :: FINTOPO6:34 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Bool "not" (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; theorem :: FINTOPO6:35 (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 "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "C")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k9_fin_topo :::"^b"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; theorem :: FINTOPO6:36 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "C")) "is" ($#v4_fin_topo :::"connected"::: ) )) "holds" (Bool (Set (Set (Var "C")) ($#k9_fin_topo :::"^b"::: ) ) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; theorem :: FINTOPO6:37 (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")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "C")))) & (Bool (Set (Var "B")) "," (Set (Var "C")) ($#r1_fintopo4 :::"are_separated"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v4_fin_topo :::"connected"::: ) ))) ; theorem :: FINTOPO6:38 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X9")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_fintopo6 :::"SubSpace"::: ) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X9")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v4_fin_topo :::"connected"::: ) ) ")" ))))) ; theorem :: FINTOPO6:39 (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 "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "A")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT")))) "holds" (Bool (Set (Var "A")) "is" ($#v3_fin_topo :::"closed"::: ) ))) ; theorem :: FINTOPO6:40 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "A")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT"))) & (Bool (Set (Var "B")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT"))) & (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_fintopo4 :::"are_separated"::: ) ))) ; theorem :: FINTOPO6:41 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "A")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT"))) & (Bool (Set (Var "B")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT"))) & (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))))) ; theorem :: FINTOPO6:42 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "C")) "is" ($#v4_fin_topo :::"connected"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" "not" (Bool (Set (Var "S")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Var "FT"))) "or" (Bool (Set (Var "C")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "S"))) "or" (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) ")" )))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); pred "B" :::"is_a_component_of"::: "A" means :: FINTOPO6:def 5 (Bool "ex" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "FT" ($#k1_fintopo6 :::"|"::: ) "A" ")" ) "st" (Bool "(" (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) "B") & (Bool (Set (Var "B1")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set "FT" ($#k1_fintopo6 :::"|"::: ) "A")) ")" )); end; :: deftheorem defines :::"is_a_component_of"::: FINTOPO6: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" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_fintopo6 :::"is_a_component_of"::: ) (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "B1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "FT")) ($#k1_fintopo6 :::"|"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "B1")) ($#r1_fintopo6 :::"is_a_component_of"::: ) (Set (Set (Var "FT")) ($#k1_fintopo6 :::"|"::: ) (Set (Var "A")))) ")" )) ")" )))); theorem :: FINTOPO6:43 (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 "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))) & (Bool (Set (Var "FT")) "is" ($#v1_fintopo6 :::"connected"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) & (Bool (Set (Var "C")) ($#r2_fintopo6 :::"is_a_component_of"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "FT")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "C"))) "is" ($#v4_fin_topo :::"connected"::: ) )))) ; begin definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "FT")); attr "f" is :::"continuous"::: means :: FINTOPO6:def 6 (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" "FT" "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x1"))))) ")" ) ")" ); end; :: deftheorem defines :::"continuous"::: FINTOPO6:def 6 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) "iff" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "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")))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "x1"))))) ")" ) ")" ) ")" ))); registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "x" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v2_fintopo6 :::"continuous"::: ) for ($#m2_finseq_1 :::"FinSequence":::) "of" "FT"; end; theorem :: FINTOPO6:44 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) "is" ($#v2_fintopo6 :::"continuous"::: ) )))) ; theorem :: FINTOPO6:45 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "g"))) "is" ($#v2_fintopo6 :::"continuous"::: ) ))) ; 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")); attr "A" is :::"arcwise_connected"::: means :: FINTOPO6:def 7 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" "FT" "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "FT" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ))); end; :: deftheorem defines :::"arcwise_connected"::: FINTOPO6: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 "(" (Bool (Set (Var "A")) "is" ($#v3_fintopo6 :::"arcwise_connected"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ))) ")" ))); registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v3_fintopo6 :::"arcwise_connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "FT"))); end; registrationlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); cluster (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) -> ($#v3_fintopo6 :::"arcwise_connected"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "FT"; end; theorem :: FINTOPO6:46 (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 "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_fin_topo :::"connected"::: ) ) "iff" (Bool (Set (Var "A")) "is" ($#v3_fintopo6 :::"arcwise_connected"::: ) ) ")" ))) ; theorem :: FINTOPO6:47 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k"))) "is" ($#v2_fintopo6 :::"continuous"::: ) )))) ; theorem :: FINTOPO6:48 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "k"))) "is" ($#v2_fintopo6 :::"continuous"::: ) )))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "g" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "FT")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "FT")); let "x1", "x2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "FT")); pred "g" :::"is_minimum_path_in"::: "A" "," "x1" "," "x2" means :: FINTOPO6:def 8 (Bool "(" (Bool "g" "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) "g") ($#r1_tarski :::"c="::: ) "A") & (Bool (Set "g" ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "x1") & (Bool (Set "g" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "g" ")" )) ($#r1_hidden :::"="::: ) "x2") & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "FT" "st" (Bool (Bool (Set (Var "h")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "x1") & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) "x2")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "g") ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) ")" ) ")" ); end; :: deftheorem defines :::"is_minimum_path_in"::: FINTOPO6:def 8 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))) "iff" (Bool "(" (Bool (Set (Var "g")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "h")))) ")" ) ")" ) ")" ))))); theorem :: FINTOPO6:49 (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")) (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 (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x")) "," (Set (Var "x")))))) ; theorem :: FINTOPO6:50 (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 "(" (Bool (Set (Var "A")) "is" ($#v3_fintopo6 :::"arcwise_connected"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "st" (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))))) ")" ))) ; theorem :: FINTOPO6:51 (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")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "st" (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))))))) ; theorem :: FINTOPO6:52 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k"))) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set "(" (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set "(" (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))) ")" )))))) ; theorem :: FINTOPO6:53 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "k"))) "is" ($#v2_fintopo6 :::"continuous"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "k")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set "(" (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))) & (Bool (Set (Set "(" (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "k")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "g")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "k")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" )))))) ; theorem :: FINTOPO6:54 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2")))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "k"))) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k"))))))))) ; theorem :: FINTOPO6:55 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2")))) "holds" (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))))) ; definitionlet "FT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "FT")); attr "f" is :::"inv_continuous"::: means :: FINTOPO6:def 9 (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "FT" "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Num 1))))) "holds" (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) ")" ) ")" ); end; :: deftheorem defines :::"inv_continuous"::: FINTOPO6:def 9 : (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_fintopo6 :::"inv_continuous"::: ) ) "iff" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "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")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_fin_topo :::"U_FT"::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k1_nat_1 :::"+"::: ) (Num 1))))) "holds" (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) ")" ) ")" ) ")" ))); theorem :: FINTOPO6:56 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v4_fintopo6 :::"inv_continuous"::: ) ))))) ; theorem :: FINTOPO6:57 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))) & (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"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 "g"))))) "holds" (Bool (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_enumset1 :::"}"::: ) )) ")" ) & (Bool (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 2) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "g")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_fin_topo :::"U_FT"::: ) (Set "(" (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "g")) ")" ) ")" ) ($#k2_tarski :::"}"::: ) )) ")" ))))) ; theorem :: FINTOPO6:58 (Bool "for" (Set (Var "FT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "FT")) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "FT")) ($#k1_fintopo6 :::"|"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r3_fintopo6 :::"is_minimum_path_in"::: ) (Set (Var "A")) "," (Set (Var "x1")) "," (Set (Var "x2"))) & (Bool (Set (Var "FT")) "is" ($#v3_orders_2 :::"filled"::: ) ) & (Bool (Set (Var "FT")) "is" ($#v1_fin_topo :::"symmetric"::: ) ) & (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x1")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (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 ($#k3_finseq_1 :::"len"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "B0")) "," (Set (Var "i")) ")" )) & "(" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "implies" (Bool "not" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k7_fintopo3 :::"Finf"::: ) "(" (Set (Var "B0")) "," (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ))) ")" ")" ))))))) ;