:: CONNSP_3 semantic presentation begin definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "V" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); func :::"Component_of"::: "V" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" means :: CONNSP_3:def 1 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "GX" "st" (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "GX" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool "V" ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" ) ")" ) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) it) ")" )); end; :: deftheorem defines :::"Component_of"::: CONNSP_3:def 1 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" ) ")" ) & (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) ")" )) ")" ))); theorem :: CONNSP_3:1 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))) "holds" (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")))))) ; theorem :: CONNSP_3:2 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" "not" (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) "or" "not" (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" )) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CONNSP_3:3 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "GX")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "GX"))))) ; theorem :: CONNSP_3:4 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CONNSP_3:5 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V"))) "is" ($#v2_connsp_1 :::"connected"::: ) ))) ; theorem :: CONNSP_3:6 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V"))) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")))))) ; theorem :: CONNSP_3:7 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) )) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: CONNSP_3:8 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) "iff" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")))) ")" )) ")" ))) ; theorem :: CONNSP_3:9 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V"))) "is" ($#v3_connsp_1 :::"a_component"::: ) ))) ; theorem :: CONNSP_3:10 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")))))) ; theorem :: CONNSP_3:11 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set "(" ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "V")))))) ; theorem :: CONNSP_3:12 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "B")))))) ; theorem :: CONNSP_3:13 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A")))))) ; theorem :: CONNSP_3:14 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A")))))) ; theorem :: CONNSP_3:15 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A"))))))) ; theorem :: CONNSP_3:16 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A")))) ")" ))) ; theorem :: CONNSP_3:17 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "A")))))) ; theorem :: CONNSP_3:18 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_connsp_3 :::"Component_of"::: ) (Set (Var "B")))))) ; begin definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; mode :::"a_union_of_components"::: "of" "GX" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" means :: CONNSP_3:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "GX" "st" (Bool "(" (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "GX" "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "B")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")))) ")" )); end; :: deftheorem defines :::"a_union_of_components"::: CONNSP_3:def 2 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool "(" (Bool "(" "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "B")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) ")" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "F")))) ")" )) ")" ))); theorem :: CONNSP_3:19 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "GX"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX")))) ; theorem :: CONNSP_3:20 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "GX"))))) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))))) ; theorem :: CONNSP_3:21 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX")))) "holds" (Bool (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; theorem :: CONNSP_3:22 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) & (Bool (Set (Var "B")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX")))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) & (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) ")" ))) ; theorem :: CONNSP_3:23 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Fu")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "Fu")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) ")" )) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "Fu"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))))) ; theorem :: CONNSP_3:24 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Fu")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "GX")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "Fu")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) ")" )) "holds" (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "Fu"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))))) ; theorem :: CONNSP_3:25 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))) & (Bool (Set (Var "B")) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "GX"))))) ; begin definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "GX")); assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set (Const "B"))) ; func :::"Down"::: "(" "p" "," "B" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" "GX" ($#k1_pre_topc :::"|"::: ) "B" ")" ) equals :: CONNSP_3:def 3 "p"; end; :: deftheorem defines :::"Down"::: CONNSP_3:def 3 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_connsp_3 :::"Down"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p")))))); definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Const "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Const "B")) ")" ); assume (Bool (Set (Const "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; func :::"Up"::: "p" -> ($#m1_subset_1 :::"Point":::) "of" "GX" equals :: CONNSP_3:def 4 "p"; end; :: deftheorem defines :::"Up"::: CONNSP_3:def 4 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_connsp_3 :::"Up"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))); definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "V", "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); func :::"Down"::: "(" "V" "," "B" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "GX" ($#k1_pre_topc :::"|"::: ) "B" ")" ) equals :: CONNSP_3:def 5 (Set "V" ($#k9_subset_1 :::"/\"::: ) "B"); end; :: deftheorem defines :::"Down"::: CONNSP_3:def 5 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool (Set ($#k4_connsp_3 :::"Down"::: ) "(" (Set (Var "V")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "V")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")))))); definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); let "V" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Const "B")) ")" ); func :::"Up"::: "V" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" equals :: CONNSP_3:def 6 "V"; end; :: deftheorem defines :::"Up"::: CONNSP_3:def 6 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "holds" (Bool (Set ($#k5_connsp_3 :::"Up"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Var "V")))))); definitionlet "GX" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "GX")); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "GX")); assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set (Const "B"))) ; func :::"Component_of"::: "(" "p" "," "B" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "GX" means :: CONNSP_3:def 7 (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" "GX" ($#k1_pre_topc :::"|"::: ) "B" ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) "p")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "q"))))); end; :: deftheorem defines :::"Component_of"::: CONNSP_3:def 7 : (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_connsp_3 :::"Component_of"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" )) "iff" (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "q"))))) ")" ))))); theorem :: CONNSP_3:26 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k6_connsp_3 :::"Component_of"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ))))) ; theorem :: CONNSP_3:27 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_connsp_3 :::"Component_of"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set "(" ($#k2_connsp_3 :::"Down"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ")" )))))) ; theorem :: CONNSP_3:28 (Bool "for" (Set (Var "GX")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set ($#k4_connsp_3 :::"Down"::: ) "(" (Set (Var "V")) "," (Set (Var "B")) ")" ) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: CONNSP_3:29 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k4_connsp_3 :::"Down"::: ) "(" (Set (Var "V")) "," (Set (Var "B")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")))))) ; theorem :: CONNSP_3:30 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k5_connsp_3 :::"Up"::: ) (Set (Var "V")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))))) ; theorem :: CONNSP_3:31 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "V")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k4_connsp_3 :::"Down"::: ) "(" (Set (Var "V")) "," (Set (Var "B")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "V")))))) ; theorem :: CONNSP_3:32 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "GX")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k4_connsp_3 :::"Down"::: ) "(" (Set "(" ($#k5_connsp_3 :::"Up"::: ) (Set (Var "V")) ")" ) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "V")))))) ; theorem :: CONNSP_3:33 (Bool "for" (Set (Var "GX")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "GX")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "GX")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_connsp_3 :::"Component_of"::: ) "(" (Set (Var "p")) "," (Set (Var "B")) ")" ) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" "T"; end; theorem :: CONNSP_3:34 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_connsp_3 :::"a_union_of_components"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ))) ;