:: CONNSP_2 semantic presentation begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); mode :::"a_neighborhood"::: "of" "x" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: CONNSP_2:def 1 (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) it)); end; :: deftheorem defines :::"a_neighborhood"::: CONNSP_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "b3")))) ")" )))); definitionlet "X" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); mode :::"a_neighborhood"::: "of" "A" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: CONNSP_2:def 2 (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) it)); end; :: deftheorem defines :::"a_neighborhood"::: CONNSP_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "b3")))) ")" ))); theorem :: CONNSP_2:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "B")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))))) ; theorem :: CONNSP_2:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "B")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) ")" ) "iff" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) ")" )))) ; theorem :: CONNSP_2:3 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "U1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U1")))) "holds" (Bool (Set (Var "U1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))))) ; theorem :: CONNSP_2:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U1")))))) ; theorem :: CONNSP_2:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U1"))) ")" ))))) ; theorem :: CONNSP_2:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "U1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) "iff" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U1"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" )) ")" )))) ; theorem :: CONNSP_2:7 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "U1")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U1")))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "U1"))) ")" ))) ")" ))) ; theorem :: CONNSP_2:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) "iff" (Bool (Set (Var "V")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) ")" )))) ; theorem :: CONNSP_2:9 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Var "A1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x1"))))))))) ; theorem :: CONNSP_2:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x1"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "A1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))))))))) ; theorem :: CONNSP_2:11 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_connsp_1 :::"a_component"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "B"))))) ; theorem :: CONNSP_2:12 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "x1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "x")))))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); pred "X" :::"is_locally_connected_in"::: "x" means :: CONNSP_2:def 3 (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" "x")) "holds" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" "x") & (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U1"))) ")" ))); end; :: deftheorem defines :::"is_locally_connected_in"::: CONNSP_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "U1")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "V")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Var "U1"))) ")" ))) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); attr "X" is :::"locally_connected"::: means :: CONNSP_2:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool "X" ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x")))); end; :: deftheorem defines :::"locally_connected"::: CONNSP_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X")) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x")))) ")" )); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); pred "A" :::"is_locally_connected_in"::: "x" means :: CONNSP_2:def 5 (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool "A" ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" "X" ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) "x") & (Bool (Set "X" ($#k1_pre_topc :::"|"::: ) (Set (Var "B"))) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x1"))) ")" ))); end; :: deftheorem defines :::"is_locally_connected_in"::: CONNSP_2:def 5 : (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B"))) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x1"))) ")" ))) ")" )))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "A" is :::"locally_connected"::: means :: CONNSP_2:def 6 (Bool (Set "X" ($#k1_pre_topc :::"|"::: ) "A") "is" ($#v1_connsp_2 :::"locally_connected"::: ) ); end; :: deftheorem defines :::"locally_connected"::: CONNSP_2:def 6 : (Bool "for" (Set (Var "X")) "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_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_connsp_2 :::"locally_connected"::: ) ) "iff" (Bool (Set (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A"))) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ) ")" ))); theorem :: CONNSP_2:13 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "V")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "V")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "S")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "V"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "S")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))) ")" ))) ; theorem :: CONNSP_2:14 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "U1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "U1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U1")))) "holds" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "U1")) ")" ) "st" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "x1")) ")" ))) ")" ))) ")" ))) ; theorem :: CONNSP_2:15 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_connsp_1 :::"a_component"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: CONNSP_2:16 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r2_connsp_2 :::"is_locally_connected_in"::: ) (Set (Var "x")))))) ; theorem :: CONNSP_2:17 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v2_connsp_2 :::"locally_connected"::: ) ))) ; theorem :: CONNSP_2:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ) "iff" (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "B")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ))) ")" )) ; theorem :: CONNSP_2:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X")) ($#k1_pre_topc :::"|"::: ) (Set (Var "E")) ")" ) "st" (Bool (Bool (Set (Var "C")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "H")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "H")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "H")))) ")" ))))) ; theorem :: CONNSP_2:20 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v10_pre_topc :::"normal"::: ) ) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "C")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "G"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" ))) ")" )) ; theorem :: CONNSP_2:21 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ) & (Bool (Set (Var "X")) "is" ($#v10_pre_topc :::"normal"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool "ex" (Set (Var "R")) "," (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "S")) "is" ($#v2_connsp_1 :::"connected"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "S")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "R"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set (Var "R")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "S"))) ")" )))) ; theorem :: CONNSP_2:22 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"qComponent_of"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "X" means :: CONNSP_2:def 7 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" "X" "st" (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool "x" ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) ")" ) & (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) it) ")" )); end; :: deftheorem defines :::"qComponent_of"::: CONNSP_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_2 :::"qComponent_of"::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) ")" ) & (Bool (Set ($#k6_setfam_1 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) ")" )) ")" )))); theorem :: CONNSP_2:23 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_connsp_2 :::"qComponent_of"::: ) (Set (Var "x")))))) ; theorem :: CONNSP_2:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_2 :::"qComponent_of"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_connsp_2 :::"qComponent_of"::: ) (Set (Var "x"))))))) ; theorem :: CONNSP_2:25 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_connsp_2 :::"qComponent_of"::: ) (Set (Var "x"))) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: CONNSP_2:26 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_connsp_1 :::"Component_of"::: ) (Set (Var "x"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_connsp_2 :::"qComponent_of"::: ) (Set (Var "x")))))) ; theorem :: CONNSP_2:27 (Bool "for" (Set (Var "T")) "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 "T")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "p")) "holds" (Bool (Set (Var "G")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A")))) ")" )))) ; theorem :: CONNSP_2:28 (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "X"))) "is" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "A"))))) ; theorem :: CONNSP_2:29 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "Y")) "being" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))))) ;