:: TSP_1 semantic presentation begin definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; redefine mode :::"SubSpace"::: "of" "Y" means :: TSP_1:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y")) & (Bool "(" "for" (Set (Var "G0")) "being" ($#m1_subset_1 :::"Subset":::) "of" it "holds" (Bool "(" (Bool (Set (Var "G0")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SubSpace"::: TSP_1:def 1 : (Bool "for" (Set (Var "Y")) "," (Set (Var "b2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "G0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b2")) "holds" (Bool "(" (Bool (Set (Var "G0")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "ex" (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 (Var "G0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" )) ")" ) ")" ) ")" ) ")" )); theorem :: TSP_1:1 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) (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"::: ) )) "holds" (Bool "ex" (Set (Var "G0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) "st" (Bool "(" (Bool (Set (Var "G0")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))) ")" ))))) ; definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; redefine mode :::"SubSpace"::: "of" "Y" means :: TSP_1:def 2 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y")) & (Bool "(" "for" (Set (Var "F0")) "being" ($#m1_subset_1 :::"Subset":::) "of" it "holds" (Bool "(" (Bool (Set (Var "F0")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SubSpace"::: TSP_1:def 2 : (Bool "for" (Set (Var "Y")) "," (Set (Var "b2")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "F0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b2")) "holds" (Bool "(" (Bool (Set (Var "F0")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) ")" )) ")" ) ")" ) ")" ) ")" )); theorem :: TSP_1:2 (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool "ex" (Set (Var "F0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) "st" (Bool "(" (Bool (Set (Var "F0")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))) ")" ))))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; redefine attr "T" is :::"T_0"::: means :: TSP_1:def 3 (Bool "(" (Bool "T" "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) ")" )) "or" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" )) ")" )) ")" ); end; :: deftheorem defines :::"T_0"::: TSP_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "T")) "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" (Bool "ex" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) ")" )) "or" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" )) ")" )) ")" ) ")" )); definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; redefine attr "Y" is :::"T_0"::: means :: TSP_1:def 4 (Bool "(" (Bool "Y" "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" (Bool "ex" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" )) ")" ); end; :: deftheorem defines :::"T_0"::: TSP_1:def 4 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "Y")) "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" (Bool "ex" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) "or" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" )) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#~v6_pre_topc "non" ($#v6_pre_topc :::"T_0"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_tdlat_3 :::"discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#~v6_pre_topc "non" ($#v6_pre_topc :::"T_0"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_pre_topc "non" ($#v6_pre_topc :::"T_0"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_pre_topc :::"T_0"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_pre_topc :::"T_0"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v2_tdlat_3 "non" ($#v2_tdlat_3 :::"anti-discrete"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); redefine attr "X" is :::"T_0"::: means :: TSP_1:def 5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"T_0"::: TSP_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) ")" )); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); redefine attr "X" is :::"T_0"::: means :: TSP_1:def 6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ")" )); end; :: deftheorem defines :::"T_0"::: TSP_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))) "or" "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) ")" )); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); redefine attr "X" is :::"T_0"::: means :: TSP_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))); end; :: deftheorem defines :::"T_0"::: TSP_1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_pre_topc :::"T_0"::: ) ($#v3_tdlat_3 :::"almost_discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tdlat_3 :::"discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) ($#v3_tdlat_3 :::"almost_discrete"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_pre_topc "non" ($#v6_pre_topc :::"T_0"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_pre_topc :::"T_0"::: ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v3_tdlat_3 "non" ($#v3_tdlat_3 :::"almost_discrete"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; definitionmode Kolmogorov_space is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_pre_topc :::"T_0"::: ) ($#l1_pre_topc :::"TopSpace":::); mode non-Kolmogorov_space is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_pre_topc "non" ($#v6_pre_topc :::"T_0"::: ) ) ($#l1_pre_topc :::"TopSpace":::); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_pre_topc :::"T_0"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#~v6_pre_topc "non" ($#v6_pre_topc :::"T_0"::: ) ) ($#~v1_tdlat_3 "non" ($#v1_tdlat_3 :::"discrete"::: ) ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; begin definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); attr "IT" is :::"T_0"::: means :: TSP_1:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ))); end; :: deftheorem defines :::"T_0"::: TSP_1:def 8 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ))) ")" ))); definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); redefine attr "A" is :::"T_0"::: means :: TSP_1:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))); end; :: deftheorem defines :::"T_0"::: TSP_1:def 9 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))) ")" ))); theorem :: TSP_1:3 (Bool "for" (Set (Var "Y0")) "," (Set (Var "Y1")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "D0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y0")) (Bool "for" (Set (Var "D1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y1")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y0"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y1"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "Y1"))) "#)" )) & (Bool (Set (Var "D0")) ($#r1_hidden :::"="::: ) (Set (Var "D1"))) & (Bool (Set (Var "D0")) "is" ($#v1_tsp_1 :::"T_0"::: ) )) "holds" (Bool (Set (Var "D1")) "is" ($#v1_tsp_1 :::"T_0"::: ) )))) ; theorem :: TSP_1:4 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool (Set (Var "Y")) "is" ($#v6_pre_topc :::"T_0"::: ) ) ")" ))) ; theorem :: TSP_1:5 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; theorem :: TSP_1:6 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "or" (Bool (Set (Var "B")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; theorem :: TSP_1:7 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ) & (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tsp_1 :::"T_0"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; theorem :: TSP_1:8 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) & (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_tsp_1 :::"T_0"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; theorem :: TSP_1:9 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_tex_2 :::"discrete"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; theorem :: TSP_1:10 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tex_4 :::"anti-discrete"::: ) ) & (Bool (Bool "not" (Set (Var "A")) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) )))) ; 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")); redefine attr "A" is :::"T_0"::: means :: TSP_1:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"T_0"::: TSP_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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) ")" ))); 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")); redefine attr "A" is :::"T_0"::: means :: TSP_1:def 11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))); end; :: deftheorem defines :::"T_0"::: TSP_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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ")" ))); 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")); redefine attr "A" is :::"T_0"::: means :: TSP_1:def 12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))); end; :: deftheorem defines :::"T_0"::: TSP_1:def 12 : (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" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "not" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))) ")" ))); theorem :: TSP_1:11 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; theorem :: TSP_1:12 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) ; begin registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v6_pre_topc :::"T_0"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y"; end; definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "Y0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "Y")); :: original: :::"T_0"::: redefine attr "Y0" is :::"T_0"::: means :: TSP_1:def 13 (Bool "(" (Bool "Y0" "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" "Y0") & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Point":::) "of" "Y0") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ))) ")" ); end; :: deftheorem defines :::"T_0"::: TSP_1:def 13 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "Y0")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "Y0")) "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y0"))) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y0"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ))) ")" ) ")" ))); definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "Y0" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "Y")); :: original: :::"T_0"::: redefine attr "Y0" is :::"T_0"::: means :: TSP_1:def 14 (Bool "(" (Bool "Y0" "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" "Y" "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" "Y0") & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Point":::) "of" "Y0") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "holds" (Bool "(" "not" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))) ")" ); end; :: deftheorem defines :::"T_0"::: TSP_1:def 14 : (Bool "for" (Set (Var "Y")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "Y0")) "is" ($#v6_pre_topc :::"T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "Y0")) "is" ($#v2_struct_0 :::"empty"::: ) ) "or" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y0"))) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y0"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool "(" "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "holds" (Bool "(" "not" (Bool (Set (Var "E")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) "or" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ))) ")" ) ")" ))); theorem :: TSP_1:13 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y0"))))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) "iff" (Bool (Set (Var "Y0")) "is" bbbadV6_PRE_TOPC()) ")" )))) ; theorem :: TSP_1:14 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) (Bool "for" (Set (Var "Y1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y1")))) "holds" (Bool (Set (Var "Y0")) "is" bbbadV6_PRE_TOPC())))) ; theorem :: TSP_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")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (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 (Set (Set (Var "X1")) ($#k2_tsep_1 :::"meet"::: ) (Set (Var "X2"))) "is" bbbadV6_PRE_TOPC())))) ; theorem :: TSP_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"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_tsep_1 :::"open"::: ) ) "or" (Bool (Set (Var "X2")) "is" ($#v1_tsep_1 :::"open"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" bbbadV6_PRE_TOPC()))) ; theorem :: TSP_1:17 (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"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "X1")) "is" ($#v1_borsuk_1 :::"closed"::: ) ) "or" (Bool (Set (Var "X2")) "is" ($#v1_borsuk_1 :::"closed"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "X1")) ($#k1_tsep_1 :::"union"::: ) (Set (Var "X2"))) "is" bbbadV6_PRE_TOPC()))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); mode Kolmogorov_subspace of "X" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TSP_1:18 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A0")) "is" ($#v1_tsp_1 :::"T_0"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"Kolmogorov_subspace":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))))) ; registrationlet "X" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v6_pre_topc :::"T_0"::: ) ($#v1_tex_2 :::"proper"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#l1_pre_topc :::"Kolmogorov_space":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#l1_pre_topc :::"non-Kolmogorov_space":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tex_2 :::"proper"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; registrationlet "X" be ($#l1_pre_topc :::"non-Kolmogorov_space":::); cluster ($#v1_pre_topc :::"strict"::: ) bbbadV6_PRE_TOPC() for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; definitionlet "X" be ($#l1_pre_topc :::"non-Kolmogorov_space":::); mode non-Kolmogorov_subspace of "X" is bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TSP_1:19 (Bool "for" (Set (Var "X")) "being" ($#l1_pre_topc :::"non-Kolmogorov_space":::) (Bool "for" (Set (Var "A0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" (Set (Var "A0")) "is" ($#v1_tsp_1 :::"T_0"::: ) ))) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"non-Kolmogorov_subspace":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))))) ;