:: TMAP_1 semantic presentation begin registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X1", "X2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); cluster (Set "X1" ($#k1_tsep_1 :::"union"::: ) "X2") -> ($#v2_pre_topc :::"TopSpace-like"::: ) ; end; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A1", "A2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A1")) "," (Set (Const "B")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A2")) "," (Set (Const "B")); assume (Bool (Set (Set (Const "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Const "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Const "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Const "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Const "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Const "A2")) ")" ))) ; func "f1" :::"union"::: "f2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "A1" ($#k4_subset_1 :::"\/"::: ) "A2" ")" ) "," "B" means :: TMAP_1:def 1 (Bool "(" (Bool (Set it ($#k2_partfun1 :::"|"::: ) "A1") ($#r1_hidden :::"="::: ) "f1") & (Bool (Set it ($#k2_partfun1 :::"|"::: ) "A2") ($#r1_hidden :::"="::: ) "f2") ")" ); end; :: deftheorem defines :::"union"::: TMAP_1:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" ) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set (Set (Var "b7")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set (Var "b7")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Var "f2"))) ")" ) ")" )))))); theorem :: TMAP_1:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_subset_1 :::"misses"::: ) (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Var "f2"))) ")" ))))) ; theorem :: TMAP_1:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")) ")" ) "," (Set (Var "B")) (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B")) (Bool "for" (Set (Var "g2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Var "g1"))) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "g2"))))))))) ; theorem :: TMAP_1:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f1")))))))) ; theorem :: TMAP_1:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "A3")) "," (Set (Var "A12")) "," (Set (Var "A23")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A12")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A23")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A2")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A3"))))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B")) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A3")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" ))) & (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f3")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A3")) ")" ))) & (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f3")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A3")) ")" )))) "holds" (Bool "for" (Set (Var "f12")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A12")) "," (Set (Var "B")) (Bool "for" (Set (Var "f23")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A23")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "f12")) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2")))) & (Bool (Set (Var "f23")) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f3"))))) "holds" (Bool (Set (Set (Var "f12")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f3"))) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f23"))))))))))) ; theorem :: TMAP_1:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A2")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "A1")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A2")))) "implies" (Bool (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f2"))) ")" & "(" (Bool (Bool (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f2")))) "implies" (Bool (Set (Var "A1")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A2"))) ")" & "(" (Bool (Bool (Set (Var "A2")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A1")))) "implies" (Bool (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f1"))) ")" & "(" (Bool (Bool (Set (Set (Var "f1")) ($#k1_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f1")))) "implies" (Bool (Set (Var "A2")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A1"))) ")" ")" ))))) ; begin theorem :: TMAP_1:6 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X0"))) "#)" ) "is" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))))) ; theorem :: TMAP_1:7 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X2"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" ))) ; theorem :: TMAP_1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "X2")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" )) ; theorem :: TMAP_1:9 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "X2")) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "X2")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) ")" )) ; theorem :: TMAP_1:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))))))) ; theorem :: TMAP_1:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "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 "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "holds" (Bool "(" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "or" (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )))) ; theorem :: TMAP_1:12 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ) "holds" (Bool "(" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) & (Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )))) ; theorem :: TMAP_1:13 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "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 "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "F1")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F2")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F2")))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "st" (Bool "(" (Bool (Set (Var "H")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "F1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "F2")))) ")" ))))))) ; theorem :: TMAP_1:14 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "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 "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) (Bool "for" (Set (Var "U1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "U2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "U1")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U1"))) & (Bool (Set (Var "U2")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "U2")))) "holds" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "U1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "U2")))) ")" ))))))) ; theorem :: TMAP_1:15 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "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 "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x1")) (Bool "for" (Set (Var "A2")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x2")) (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "V")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "A2")))) ")" ))))))))) ; theorem :: TMAP_1:16 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "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 "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "for" (Set (Var "A1")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x1")) (Bool "for" (Set (Var "A2")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x2")) (Bool "ex" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "st" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "A2")))))))))))) ; theorem :: TMAP_1:17 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "holds" (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) & (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) ")" ))) ; theorem :: TMAP_1:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) ")" ))) ; theorem :: TMAP_1:19 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) ")" ))) ; theorem :: TMAP_1:20 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X0")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X0"))) "#)" )))) ; theorem :: TMAP_1:21 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X0"))) "#)" )))) ; theorem :: TMAP_1:22 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y1")) "," (Set (Var "X1")) "," (Set (Var "Y2")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))))) ; theorem :: TMAP_1:23 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "Y2"))) & (Bool (Set (Var "Y1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Var "Y2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))))) ; theorem :: TMAP_1:24 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))))) ; theorem :: TMAP_1:25 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))))) ; theorem :: TMAP_1:26 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) ")" ) & (Bool "(" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) ")" )) "implies" (Bool "(" (Bool (Set (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) & (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) ")" ) & (Bool "(" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) ")" )) "implies" (Bool "(" (Bool (Set (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) & (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1")))) ")" ) ")" ")" ))) ; theorem :: TMAP_1:27 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" & "(" (Bool (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0")))) ")" ")" ))) ; theorem :: TMAP_1:28 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "or" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" )) & (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" )) ")" ))) ; theorem :: TMAP_1:29 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "implies" (Bool "(" (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) & (Bool (Set (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "implies" (Bool "(" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X0"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) ")" ) ")" ")" ))) ; theorem :: TMAP_1:30 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y2"))) & (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "Y2"))) "or" (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "Y2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) ")" ))) ; theorem :: TMAP_1:31 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "X2")) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")))) & (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Set (Var "Y2")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "Y2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ))) ; theorem :: TMAP_1:32 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "X2")) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X0")))) & (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Set (Var "Y2")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))))) "holds" (Bool "(" (Bool (Set (Var "Y1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "Y2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ))) ; theorem :: TMAP_1:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) & (Bool (Set (Var "X1")) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "X2")) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" (Bool "not" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))))) & (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2")) ")" ) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X0")))) & (Bool (Set (Set (Var "Y1")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) & (Bool (Set (Set (Var "Y2")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) & (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))))) "holds" (Bool "(" (Bool (Set (Set (Var "Y1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "Y2"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ))) ; theorem :: TMAP_1:34 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" "not" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) ")" ) & "(" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) ")" )) "implies" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) ")" & (Bool "(" "not" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) ")" ) & "(" (Bool (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) ")" )) "implies" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ")" ))) ; theorem :: TMAP_1:35 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0")))) "implies" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0")))) "implies" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) ")" & "(" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "implies" (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) & (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) & (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "implies" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) ")" ")" ))) ; theorem :: TMAP_1:36 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0")))) "implies" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) & (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X0"))) ")" ) ")" & "(" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))))) "implies" (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1"))) & (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2"))) ")" ) ")" ")" ))) ; theorem :: TMAP_1:37 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "(" "(" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) "or" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) ")" )) "implies" (Bool (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X0"))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1"))) "or" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) ")" )) "implies" (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")))) ")" ")" ))) ; theorem :: TMAP_1:38 (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 "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1")))) "holds" (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1"))) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))))) ; theorem :: TMAP_1:39 (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 "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X1")))) "holds" (Bool (Set (Set (Var "X0")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X1"))) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))))) ; theorem :: TMAP_1:40 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X1")))) ")" )))) ; theorem :: TMAP_1:41 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X2")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X1")))) ")" )))) ; begin definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); pred "f" :::"is_continuous_at"::: "x" means :: TMAP_1:def 2 (Bool "for" (Set (Var "G")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set "f" ($#k3_funct_2 :::"."::: ) "x") (Bool "ex" (Set (Var "H")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" "x" "st" (Bool (Set "f" ($#k7_relset_1 :::".:"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))); end; :: deftheorem defines :::"is_continuous_at"::: TMAP_1:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) (Bool "ex" (Set (Var "H")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")) "st" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Var "G"))))) ")" )))); notationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); antonym "f" :::"is_not_continuous_at"::: "x" for "f" :::"is_continuous_at"::: "x"; end; theorem :: TMAP_1:42 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "G"))) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x")))) ")" )))) ; theorem :: TMAP_1:43 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "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 "x")) ($#r2_hidden :::"in"::: ) (Set (Var "H"))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set (Var "G"))) ")" ))) ")" )))) ; theorem :: TMAP_1:44 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))) ")" ))) ; theorem :: TMAP_1:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Z"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))))))) ; theorem :: TMAP_1:46 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))))))) ; theorem :: TMAP_1:47 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))))))) ; theorem :: TMAP_1:48 (Bool "for" (Set (Var "Z")) "," (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "y")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))))))) ; theorem :: TMAP_1:49 (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))))))) ; theorem :: TMAP_1:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))) ")" ))) ; theorem :: TMAP_1:51 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Z")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Z"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z"))))) ; theorem :: TMAP_1:52 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z"))))) ; definitionlet "S", "T" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); let "R" be ($#l1_struct_0 :::"1-sorted"::: ) ; assume (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S")))) ; func "f" :::"|"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" "R" "," "T" equals :: TMAP_1:def 3 (Set "f" ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; :: deftheorem defines :::"|"::: TMAP_1:def 3 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) (Bool "for" (Set (Var "R")) "being" ($#l1_struct_0 :::"1-sorted"::: ) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))))); definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "X0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); redefine func "f" :::"|"::: "X0" equals :: TMAP_1:def 4 (Set "f" ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X0")); end; :: deftheorem defines :::"|"::: TMAP_1:def 4 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))))))); theorem :: TMAP_1:53 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f0")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f0"))))))) ; theorem :: TMAP_1:54 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X0"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ))) "holds" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))))))) ; theorem :: TMAP_1:55 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))))))) ; theorem :: TMAP_1:56 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "B")))))))) ; theorem :: TMAP_1:57 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Set (Set (Var "h")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))))) ; theorem :: TMAP_1:58 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X0")) "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 "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x0"))) & (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0")))))))) ; theorem :: TMAP_1:59 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (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")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) ")" ))))))) ; theorem :: TMAP_1:60 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (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")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) ")" ))))))) ; theorem :: TMAP_1:61 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#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 "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x0")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) ")" )))))) ; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "X0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); cluster (Set "f" ($#k2_tmap_1 :::"|"::: ) "X0") -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TMAP_1:62 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0")) ")" ))))))) ; theorem :: TMAP_1:63 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))))) ; theorem :: TMAP_1:64 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Z"))))))) ; definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0", "X1" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X0")) "," (Set (Const "Y")); assume (Bool (Set (Const "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X0"))) ; func "g" :::"|"::: "X1" -> ($#m1_subset_1 :::"Function":::) "of" "X1" "," "Y" equals :: TMAP_1:def 5 (Set "g" ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1")); end; :: deftheorem defines :::"|"::: TMAP_1:def 5 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))))))); theorem :: TMAP_1:65 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x0"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x0")))))))) ; theorem :: TMAP_1:66 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x0"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x0")))) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "g1"))))))) ; theorem :: TMAP_1:67 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X0"))))))) ; theorem :: TMAP_1:68 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))))))) ; theorem :: TMAP_1:69 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))))) "holds" (Bool (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "B")))))))) ; theorem :: TMAP_1:70 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0")))) & (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1")))))))) ; theorem :: TMAP_1:71 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))))))) ; theorem :: TMAP_1:72 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))))))) ; theorem :: TMAP_1:73 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X0")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f0"))) "iff" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f0"))) ")" )))))) ; theorem :: TMAP_1:74 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1")))))))) ; theorem :: TMAP_1:75 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1")))))))) ; theorem :: TMAP_1:76 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "x0"))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) "iff" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) ")" ))))))) ; theorem :: TMAP_1:77 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) "iff" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) ")" ))))))) ; theorem :: TMAP_1:78 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) "iff" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) ")" ))))))) ; theorem :: TMAP_1:79 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) "iff" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) ")" )))))) ; theorem :: TMAP_1:80 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))) "iff" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) ")" )))))) ; theorem :: TMAP_1:81 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X1"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Var "X0")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "st" (Bool (Bool (Set (Var "x0")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1")))) "holds" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0")))))))) ; theorem :: TMAP_1:82 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")))))) ; theorem :: TMAP_1:83 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X0")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")))))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k3_struct_0 :::"id"::: ) "X") -> ($#v5_pre_topc :::"continuous"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); func :::"incl"::: "X0" -> ($#m1_subset_1 :::"Function":::) "of" "X0" "," "X" equals :: TMAP_1:def 6 (Set (Set "(" ($#k3_struct_0 :::"id"::: ) "X" ")" ) ($#k2_tmap_1 :::"|"::: ) "X0"); end; :: deftheorem defines :::"incl"::: TMAP_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_tmap_1 :::"incl"::: ) (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_struct_0 :::"id"::: ) (Set (Var "X")) ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0")))))); notationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); synonym "X0" :::"incl"::: "X" for :::"incl"::: "X0"; end; theorem :: TMAP_1:84 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Set "(" ($#k4_tmap_1 :::"incl"::: ) (Set (Var "X0")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: TMAP_1:85 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f0")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k4_tmap_1 :::"incl"::: ) (Set (Var "X0"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f0")))))) ; theorem :: TMAP_1:86 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_tmap_1 :::"incl"::: ) (Set (Var "X0")) ")" )))))) ; theorem :: TMAP_1:87 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_tmap_1 :::"incl"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set (Var "X"))))) ; begin 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")); func "A" :::"-extension_of_the_topology_of"::: "X" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "X" equals :: TMAP_1:def 7 "{" (Set "(" (Set (Var "H")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k9_subset_1 :::"/\"::: ) "A" ")" ) ")" ) where H, G "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "X")) & (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "X")) ")" ) "}" ; end; :: deftheorem defines :::"-extension_of_the_topology_of"::: TMAP_1:def 7 : (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 (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "H")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" ) ")" ) where H, G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) ")" ) "}" ))); theorem :: TMAP_1:88 (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 "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))))) ; theorem :: TMAP_1:89 (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 "(" (Set (Var "G")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" ) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) "}" ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))))) ; theorem :: TMAP_1:90 (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 "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) & (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "G")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" ) where G "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) "}" )) "holds" (Bool "(" (Bool (Set (Set (Var "C")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))) ")" ))) ; theorem :: TMAP_1:91 (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 (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))))) ; theorem :: TMAP_1:92 (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 "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X")))) "iff" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (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")); func "X" :::"modified_with_respect_to"::: "A" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) equals :: TMAP_1:def 8 (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "(" "A" ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) "X" ")" ) "#)" ); end; :: deftheorem defines :::"modified_with_respect_to"::: TMAP_1:def 8 : (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 (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "(" (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")) ")" ) "#)" )))); registrationlet "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")); cluster (Set "X" ($#k6_tmap_1 :::"modified_with_respect_to"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: TMAP_1:93 (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 "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))) ")" ))) ; theorem :: TMAP_1:94 (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 "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: TMAP_1:95 (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 "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")))) ")" ))) ; 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")); func :::"modid"::: "(" "X" "," "A" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" "X" ($#k6_tmap_1 :::"modified_with_respect_to"::: ) "A" ")" ) equals :: TMAP_1:def 9 (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; :: deftheorem defines :::"modid"::: TMAP_1:def 9 : (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 ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))))); theorem :: TMAP_1:96 (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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x")))))) ; theorem :: TMAP_1:97 (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 "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "holds" (Bool (Set (Set "(" ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))))))) ; theorem :: TMAP_1:98 (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 "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "holds" (Bool (Set (Set "(" ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0"))))))) ; theorem :: TMAP_1:99 (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 "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set "(" (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")) ")" ))))) ; theorem :: TMAP_1:100 (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 "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set "(" (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")) ")" ))))) ; theorem :: TMAP_1:101 (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 "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool (Set ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A")) ")" )) ")" ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); func "X" :::"modified_with_respect_to"::: "X0" -> ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) means :: TMAP_1:def 10 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X0"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set "X" ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A"))))); end; :: deftheorem defines :::"modified_with_respect_to"::: TMAP_1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#v1_pre_topc :::"strict"::: ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "A"))))) ")" )))); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); cluster (Set "X" ($#k8_tmap_1 :::"modified_with_respect_to"::: ) "X0") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ; end; theorem :: TMAP_1:102 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set "(" (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_tmap_1 :::"-extension_of_the_topology_of"::: ) (Set (Var "X")))) ")" ) ")" ))) ; theorem :: TMAP_1:103 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0"))) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Var "Y0")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0"))))))) ; theorem :: TMAP_1:104 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "X"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")))) ")" ))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); func :::"modid"::: "(" "X" "," "X0" ")" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" "X" ($#k8_tmap_1 :::"modified_with_respect_to"::: ) "X0" ")" ) means :: TMAP_1:def 11 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X0"))) "holds" (Bool it ($#r1_funct_2 :::"="::: ) (Set ($#k7_tmap_1 :::"modid"::: ) "(" "X" "," (Set (Var "A")) ")" ))); end; :: deftheorem defines :::"modid"::: TMAP_1:def 11 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool (Set (Var "b3")) ($#r1_funct_2 :::"="::: ) (Set ($#k7_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ))) ")" )))); theorem :: TMAP_1:105 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set (Var "X")))))) ; theorem :: TMAP_1:106 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1")))) "holds" (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) "holds" (Bool (Set (Set "(" ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1")))))) ; theorem :: TMAP_1:107 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "holds" (Bool (Set (Set "(" ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x0")))))) ; theorem :: TMAP_1:108 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "," (Set (Var "X1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X1")))) "holds" (Bool (Set (Set "(" ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set "(" (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")) ")" )))) ; theorem :: TMAP_1:109 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X0"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X0")) "," (Set "(" (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")) ")" )))) ; theorem :: TMAP_1:110 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set ($#k9_tmap_1 :::"modid"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" (Set (Var "X")) ($#k8_tmap_1 :::"modified_with_respect_to"::: ) (Set (Var "X0")) ")" )) ")" ))) ; begin theorem :: TMAP_1:111 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x2"))) ")" ) ")" ))))))) ; theorem :: TMAP_1:112 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "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 "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x2"))) ")" ) ")" ))))))) ; theorem :: TMAP_1:113 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "holds" (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")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x1"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r1_tmap_1 :::"is_continuous_at"::: ) (Set (Var "x2"))) ")" ) ")" ))))))) ; theorem :: TMAP_1:114 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:115 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:116 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:117 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:118 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:119 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:120 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:121 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:122 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y"))) ")" ) ")" )))) ; theorem :: TMAP_1:123 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")))) "holds" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")))) ")" ) ")" ) ")" ))) ; theorem :: TMAP_1:124 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" )) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")))) ")" ) ")" ) ")" ))) ; theorem :: TMAP_1:125 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ")" ) ")" ) ")" ))) ; begin definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X1", "X2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X1")) "," (Set (Const "Y")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X2")) "," (Set (Const "Y")); assume (Bool "(" (Bool (Set (Const "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Const "X2"))) "or" (Bool (Set (Set (Const "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Const "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Const "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Const "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Const "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Const "X2")) ")" ))) ")" ) ; func "f1" :::"union"::: "f2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "X1" ($#k1_tsep_1 :::"union"::: ) "X2" ")" ) "," "Y" means :: TMAP_1:def 12 (Bool "(" (Bool (Set it ($#k3_tmap_1 :::"|"::: ) "X1") ($#r2_funct_2 :::"="::: ) "f1") & (Bool (Set it ($#k3_tmap_1 :::"|"::: ) "X2") ($#r2_funct_2 :::"="::: ) "f2") ")" ); end; :: deftheorem defines :::"union"::: TMAP_1:def 12 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "or" (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set (Set (Var "b7")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set (Var "b7")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" )))))); theorem :: TMAP_1:126 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y")) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1")) ")" ) ($#k10_tmap_1 :::"union"::: ) (Set "(" (Set (Var "g")) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2")) ")" )))))) ; theorem :: TMAP_1:127 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Var "g")) ($#r1_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X1")) ")" ) ($#k10_tmap_1 :::"union"::: ) (Set "(" (Set (Var "g")) ($#k2_tmap_1 :::"|"::: ) (Set (Var "X2")) ")" )))))) ; theorem :: TMAP_1:128 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) "iff" (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ))) ")" ))))) ; theorem :: TMAP_1:129 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2")))) "implies" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f2"))) ")" & "(" (Bool (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f2")))) "implies" (Bool (Set (Var "X1")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X2"))) ")" & "(" (Bool (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1")))) "implies" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f1"))) ")" & "(" (Bool (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Var "f1")))) "implies" (Bool (Set (Var "X2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X1"))) ")" ")" ))))) ; theorem :: TMAP_1:130 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "or" (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f1")))))))) ; theorem :: TMAP_1:131 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X3")) "," (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) "or" (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ))) ")" ) & (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X3"))) "or" (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f3")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3")) ")" ))) ")" ) & (Bool "(" (Bool (Set (Var "X2")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X3"))) "or" (Bool (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f3")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X2")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X3")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f3"))) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set "(" (Set (Var "f2")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f3")) ")" )))))))) ; theorem :: TMAP_1:132 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" ))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:133 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:134 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:135 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"meets"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f2")) ($#k3_tmap_1 :::"|"::: ) (Set "(" (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:136 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:137 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:138 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r3_tsep_1 :::"are_separated"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X1")) ($#r1_tsep_1 :::"misses"::: ) (Set (Var "X2"))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "Y"))))) ")" ) ")" ) ")" ))) ; theorem :: TMAP_1:139 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))))) "holds" (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) & (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_tsep_1 :::"are_weakly_separated"::: ) )) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:140 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))))) ; theorem :: TMAP_1:141 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "f1")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f2")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X2")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2")))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2")) ")" ) ($#k3_tmap_1 :::"|"::: ) (Set (Var "X2"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k10_tmap_1 :::"union"::: ) (Set (Var "f2"))) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))))) ;