:: TSP_2 semantic presentation 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")); redefine attr "A" is :::"T_0"::: means :: TSP_2:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "b"))))); end; :: deftheorem defines :::"T_0"::: TSP_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a"))) ($#r1_subset_1 :::"misses"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "b"))))) ")" ))); 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_2:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set "A" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))); end; :: deftheorem defines :::"T_0"::: TSP_2:def 2 : (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 "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#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_2:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool "ex" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "D")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ) & (Bool (Set "A" ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" ))); end; :: deftheorem defines :::"T_0"::: TSP_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "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 "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "D")) "is" ($#v3_tex_4 :::"maximal_anti-discrete"::: ) ) & (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ")" ))); definitionlet "Y" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "Y")); attr "IT" is :::"maximal_T_0"::: means :: TSP_2:def 4 (Bool "(" (Bool "IT" "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool "IT" ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool "IT" ($#r1_hidden :::"="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"maximal_T_0"::: TSP_2:def 4 : (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_2 :::"maximal_T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "D")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool (Set (Var "IT")) ($#r1_tarski :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))); theorem :: TSP_2:1 (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_2 :::"maximal_T_0"::: ) )) "holds" (Bool (Set (Var "D1")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "M" is :::"maximal_T_0"::: means :: TSP_2:def 5 (Bool "(" (Bool "M" "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) "M") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) ")" ); end; :: deftheorem defines :::"maximal_T_0"::: TSP_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_tsp_1 :::"T_0"::: ) ) & (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" ) ")" ))); theorem :: TSP_2:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v1_tops_1 :::"dense"::: ) ))) ; theorem :: TSP_2:3 (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")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) & (Bool (Set (Var "A")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) "holds" (Bool "not" (Bool (Set (Var "A")) "is" ($#v1_subset_1 :::"proper"::: ) )))) ; theorem :: TSP_2:4 (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 (Bool "not" (Set (Var "A")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )))) ; theorem :: TSP_2:5 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" )))))) ; theorem :: TSP_2:6 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")) ")" )))))) ; theorem :: TSP_2:7 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" )))))) ; theorem :: TSP_2:8 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set "(" (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" )))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); redefine attr "M" is :::"maximal_T_0"::: means :: TSP_2:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "M") & (Bool (Set "M" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" ))); end; :: deftheorem defines :::"maximal_T_0"::: TSP_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ")" ))) ")" ))); theorem :: TSP_2: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")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_tsp_1 :::"T_0"::: ) )) "holds" (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) ) ")" )))) ; theorem :: TSP_2:10 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "M")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) ))) ; begin definitionlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "IT" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "Y")); attr "IT" is :::"maximal_T_0"::: means :: TSP_2:def 7 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "Y" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT"))) "holds" (Bool (Set (Var "A")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )); end; :: deftheorem defines :::"maximal_T_0"::: TSP_2:def 7 : (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) "iff" (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 "IT"))))) "holds" (Bool (Set (Var "A")) "is" ($#v1_tsp_2 :::"maximal_T_0"::: ) )) ")" ))); theorem :: TSP_2:11 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "Y0")) "being" ($#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_2 :::"maximal_T_0"::: ) ) "iff" (Bool (Set (Var "Y0")) "is" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) ")" )))) ; registrationlet "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tsp_2 :::"maximal_T_0"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() for ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y"; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v2_tsp_2 "non" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "Y"; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Const "X")); redefine attr "X0" is :::"maximal_T_0"::: means :: TSP_2:def 8 (Bool "(" (Bool "X0" "is" bbbadV6_PRE_TOPC()) & (Bool "(" "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" "X" "st" (Bool (Bool "X0" "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y0")))) "holds" (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X0") "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" "X0") "#)" ) ($#r1_hidden :::"="::: ) (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"))) "#)" )) ")" ) ")" ); end; :: deftheorem defines :::"maximal_T_0"::: TSP_2:def 8 : (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" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X0")) "is" bbbadV6_PRE_TOPC()) & (Bool "(" "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "Y0")))) "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"))) "#)" ) ($#r1_hidden :::"="::: ) (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"))) "#)" )) ")" ) ")" ) ")" ))); theorem :: TSP_2:12 (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_2 :::"maximal_T_0"::: ) )) "holds" (Bool "ex" (Set (Var "X0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "X0")) "is" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) & (Bool (Set (Var "A0")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v2_tsp_2 :::"maximal_T_0"::: ) -> ($#v1_tex_3 :::"dense"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#~v1_tex_3 "non" ($#v1_tex_3 :::"dense"::: ) ) -> ($#~v2_tsp_2 "non" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tsep_1 :::"open"::: ) ($#v2_tsp_2 :::"maximal_T_0"::: ) -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tsep_1 :::"open"::: ) ($#v1_tex_2 :::"proper"::: ) -> ($#~v2_tsp_2 "non" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_2 :::"proper"::: ) ($#v2_tsp_2 :::"maximal_T_0"::: ) -> ($#~v1_tsep_1 "non" ($#v1_tsep_1 :::"open"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_borsuk_1 :::"closed"::: ) ($#v2_tsp_2 :::"maximal_T_0"::: ) -> ($#~v1_tex_2 "non" ($#v1_tex_2 :::"proper"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_borsuk_1 :::"closed"::: ) ($#v1_tex_2 :::"proper"::: ) -> ($#~v2_tsp_2 "non" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; cluster ($#v1_tex_2 :::"proper"::: ) ($#v2_tsp_2 :::"maximal_T_0"::: ) -> ($#~v1_borsuk_1 "non" ($#v1_borsuk_1 :::"closed"::: ) ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TSP_2:13 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y0")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) bbbadV6_PRE_TOPC() ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "X0")) "being" ($#v1_pre_topc :::"strict"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y0")) "is" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X0"))) & (Bool (Set (Var "X0")) "is" ($#v2_tsp_2 :::"maximal_T_0"::: ) ) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_tsp_2 :::"maximal_T_0"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); mode maximal_Kolmogorov_subspace of "X" is ($#v2_tsp_2 :::"maximal_T_0"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" "X"; end; theorem :: TSP_2:14 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "G0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "G0")) ($#r1_hidden :::"="::: ) (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "G0")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "G"))) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Set (Var "G0")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "G")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) ")" ) ")" ))))) ; theorem :: TSP_2:15 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_pre_topc :::"open"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "G")))) & (Bool "ex" (Set (Var "G0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "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 "X0"))))) ")" )) ")" ) ")" )))) ; theorem :: TSP_2:16 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "F0")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Var "F0")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "F"))) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "F0")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "F")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) ")" ) ")" ))))) ; theorem :: TSP_2:17 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_pre_topc :::"closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "F")))) & (Bool "ex" (Set (Var "F0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "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 "X0"))))) ")" )) ")" ) ")" )))) ; begin theorem :: TSP_2:18 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "r")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "r")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0"))))))) ; theorem :: TSP_2:19 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "r")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "r")) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")))))) ; theorem :: TSP_2: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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "r")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "r")) "is" ($#v3_borsuk_1 :::"being_a_retraction"::: ) ))))) ; theorem :: TSP_2: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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "r")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "r")) "is" ($#v3_borsuk_1 :::"being_a_retraction"::: ) )))) ; theorem :: TSP_2:22 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "r")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "st" (Bool (Set (Var "r")) "is" ($#v3_borsuk_1 :::"being_a_retraction"::: ) )))) ; theorem :: TSP_2:23 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X0")) ($#r1_borsuk_1 :::"is_a_retract_of"::: ) (Set (Var "X"))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"maximal_Kolmogorov_subspace":::) "of" (Set (Const "X")); func :::"Stone-retraction"::: "(" "X" "," "X0" ")" -> ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" "X" "," "X0" means :: TSP_2:def 9 (Bool it "is" ($#v3_borsuk_1 :::"being_a_retraction"::: ) ); end; :: deftheorem defines :::"Stone-retraction"::: TSP_2:def 9 : (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" )) "iff" (Bool (Set (Var "b3")) "is" ($#v3_borsuk_1 :::"being_a_retraction"::: ) ) ")" )))); theorem :: TSP_2:24 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: TSP_2:25 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")))))))) ; theorem :: TSP_2:26 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X0")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "E")))))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"maximal_Kolmogorov_subspace":::) "of" (Set (Const "X")); redefine func :::"Stone-retraction"::: "(" "X" "," "X0" ")" means :: TSP_2:def 10 (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X0"))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_domain_1 :::"}"::: ) )))); end; :: deftheorem defines :::"Stone-retraction"::: TSP_2: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" )) "iff" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) ")" )))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"maximal_Kolmogorov_subspace":::) "of" (Set (Const "X")); redefine func :::"Stone-retraction"::: "(" "X" "," "X0" ")" means :: TSP_2:def 11 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "X" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"Stone-retraction"::: TSP_2: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a"))))) ")" )))); theorem :: TSP_2:27 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a"))))))) ; theorem :: TSP_2:28 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k4_tex_4 :::"MaxADSet"::: ) (Set (Var "a")) ")" )))))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "X0" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"maximal_Kolmogorov_subspace":::) "of" (Set (Const "X")); redefine func :::"Stone-retraction"::: "(" "X" "," "X0" ")" means :: TSP_2:def 12 (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X0"))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set it ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))))); end; :: deftheorem defines :::"Stone-retraction"::: TSP_2:def 12 : (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X0")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" )) "iff" (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X0"))))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")))))) ")" )))); theorem :: TSP_2:29 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k8_relset_1 :::"""::: ) (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A"))))))) ; theorem :: TSP_2:30 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k3_tex_4 :::"MaxADSet"::: ) (Set (Var "A")) ")" )))))) ; theorem :: TSP_2:31 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")) ")" )))))) ; theorem :: TSP_2:32 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) "or" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")) ")" )))))) ; theorem :: TSP_2:33 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) "or" (Bool (Set (Var "B")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")) ")" )))))) ; theorem :: TSP_2:34 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v3_pre_topc :::"open"::: ) )))) ; theorem :: TSP_2:35 (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 :::"maximal_Kolmogorov_subspace":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_tsp_2 :::"Stone-retraction"::: ) "(" (Set (Var "X")) "," (Set (Var "X0")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v4_pre_topc :::"closed"::: ) )))) ;