:: COMPACT1  semantic presentation begin  definitionlet "X" be   ($#l1_pre_topc :::"TopSpace":::); let "P" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "P" is  :::"compact":::  means :: COMPACT1:def 1 (Bool  "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  "P")) "holds"  (Bool (Set (Var "U")) "is"   ($#v2_compts_1 :::"compact"::: )  )); end; 





:: deftheorem    defines :::"compact"::: COMPACT1:def 1 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v1_compact1 :::"compact"::: )  ) "iff" (Bool  "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "U"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "U")) "is"   ($#v2_compts_1 :::"compact"::: )  ))  ")" ))); 
 definitionlet "X" be   ($#l1_pre_topc :::"TopSpace":::); let "U" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "U" is  :::"relatively-compact":::  means :: COMPACT1:def 2 (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  "U") "is"   ($#v2_compts_1 :::"compact"::: )  ); end; 





:: deftheorem    defines :::"relatively-compact"::: COMPACT1:def 2 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "U")) "is"   ($#v2_compact1 :::"relatively-compact"::: )  ) "iff" (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "U"))) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" ))); 
 registrationlet "X" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v2_compact1 :::"relatively-compact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X"))); 
end; registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v2_compact1 :::"relatively-compact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))); 
end; registrationlet "X" be   ($#l1_pre_topc :::"TopSpace":::); let "U" be   ($#v2_compact1 :::"relatively-compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); 
cluster (Set   ($#k2_pre_topc :::"Cl"::: )  "U") ->   ($#v2_compts_1 :::"compact"::: )   ; 
end; notationlet "X" be   ($#l1_pre_topc :::"TopSpace":::); let "U" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); synonym  :::"pre-compact"::: "U" for  :::"relatively-compact"::: ; end; notationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"liminally-compact"::: "X" for  :::"locally-compact"::: ; end; definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); redefine attr "X" is  :::"locally-compact":::  means :: COMPACT1:def 3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" (Bool  "ex" (Set (Var "B")) "being"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "B")) "is"   ($#v1_compact1 :::"compact"::: )  ))); end; 




:: deftheorem    defines :::"liminally-compact"::: COMPACT1:def 3 :  (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_waybel_3 :::"liminally-compact"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "B")) "being"    ($#m1_yellow13 :::"basis"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "B")) "is"   ($#v1_compact1 :::"compact"::: )  )))  ")" )); 
 definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); attr "X" is  :::"locally-relatively-compact":::  means :: COMPACT1:def 4 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" (Bool  "ex" (Set (Var "U")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "U")) "is"   ($#v2_compact1 :::"relatively-compact"::: )  ))); end; 




:: deftheorem    defines :::"locally-relatively-compact"::: COMPACT1:def 4 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_compact1 :::"locally-relatively-compact"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "U")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "U")) "is"   ($#v2_compact1 :::"relatively-compact"::: )  )))  ")" )); 
 definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); attr "X" is  :::"locally-closed/compact":::  means :: COMPACT1:def 5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" (Bool  "ex" (Set (Var "U")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) "st"  (Bool  "("  (Bool (Set (Var "U")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "U")) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" ))); end; 




:: deftheorem    defines :::"locally-closed/compact"::: COMPACT1: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"   ($#v4_compact1 :::"locally-closed/compact"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "U")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) "st"  (Bool  "("  (Bool (Set (Var "U")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "U")) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" )))  ")" )); 
 definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); attr "X" is  :::"locally-compact":::  means :: COMPACT1:def 6 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" (Bool  "ex" (Set (Var "U")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "U")) "is"   ($#v2_compts_1 :::"compact"::: )  ))); end; 




:: deftheorem    defines :::"locally-compact"::: COMPACT1: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"   ($#v5_compact1 :::"locally-compact"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "U")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "x")) "st" (Bool (Set (Var "U")) "is"   ($#v2_compts_1 :::"compact"::: )  )))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v6_waybel_3 :::"liminally-compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_compact1 :::"locally-compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v9_pre_topc :::"regular"::: )     ($#v5_compact1 :::"locally-compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v9_pre_topc :::"regular"::: )     ($#v6_waybel_3 :::"liminally-compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_compact1 :::"locally-relatively-compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_compact1 :::"locally-closed/compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v4_compact1 :::"locally-closed/compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_compact1 :::"locally-relatively-compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_compact1 :::"locally-relatively-compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_compact1 :::"locally-compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v8_pre_topc :::"Hausdorff"::: )     ($#v5_compact1 :::"locally-compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_pre_topc :::"Hausdorff"::: )     ($#v3_compact1 :::"locally-relatively-compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v1_compts_1 :::"compact"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_compact1 :::"locally-compact"::: )    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"::: )   )    ($#v5_compact1 :::"locally-compact"::: )    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"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_compact1 :::"locally-compact"::: )    ($#l1_pre_topc :::"TopSpace":::); let "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); 
cluster (Set "X"  ($#k1_pre_topc :::"|"::: )  "C") ->   ($#v5_compact1 :::"locally-compact"::: )   ; 
end; registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v9_pre_topc :::"regular"::: )     ($#v5_compact1 :::"locally-compact"::: )    ($#l1_pre_topc :::"TopSpace":::); let "P" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); 
cluster (Set "X"  ($#k1_pre_topc :::"|"::: )  "P") ->   ($#v5_compact1 :::"locally-compact"::: )   ; 
end; 
theorem :: COMPACT1:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_pre_topc :::"Hausdorff"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "E"))) "is"   ($#v1_tex_3 :::"dense"::: )  ) & (Bool (Set (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "E"))) "is"   ($#v5_compact1 :::"locally-compact"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "E"))) "is"   ($#v1_tsep_1 :::"open"::: )  ))) ; 
 
theorem :: COMPACT1:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 definitionlet "X", "Y" be   ($#l1_pre_topc :::"TopSpace":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "f" is  :::"embedding":::  means :: COMPACT1:def 7 (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set  "(" "Y"  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  "f" ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  "f") & (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )  ")" )); end; 






:: deftheorem    defines :::"embedding"::: COMPACT1:def 7 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v6_compact1 :::"embedding"::: )  ) "iff" (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  "(" (Set (Var "Y"))  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )  ")" ))  ")" ))); 
 
theorem :: COMPACT1:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")))) & (Bool  "ex" (Set (Var "Xy")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st"  (Bool  "("  (Bool (Set (Var "Xy"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "(" (Set (Var "Y"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Xy")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X"))))  ")" ))) "holds"  (Bool (Set   ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "is"   ($#v6_compact1 :::"embedding"::: )  )) ; 
 definitionlet "X", "Y" be   ($#l1_pre_topc :::"TopSpace":::); let "h" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "h" is  :::"compactification":::  means :: COMPACT1:def 8 (Bool  "("  (Bool "h" "is"   ($#v6_compact1 :::"embedding"::: )  ) & (Bool "Y" "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set "h"  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "X" ")" )) "is"   ($#v1_tops_1 :::"dense"::: )  )  ")" ); end; 






:: deftheorem    defines :::"compactification"::: COMPACT1:def 8 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"   (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v7_compact1 :::"compactification"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v6_compact1 :::"embedding"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set (Set (Var "h"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")) ")" )) "is"   ($#v1_tops_1 :::"dense"::: )  )  ")" )  ")" ))); 
 registrationlet "X", "Y" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y"))   ($#v7_compact1 :::"compactification"::: )    ->   ($#v6_compact1 :::"embedding"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Y"))))); 
end; definitionlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"One-Point_Compactification"::: "X" ->   ($#v1_pre_topc :::"strict"::: )     ($#l1_pre_topc :::"TopStruct"::: )   means :: COMPACT1:def 9 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "X" ")" ))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "X")  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  "(" (Set (Var "U"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "X" ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) where U "is"   ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool  "("  (Bool (Set (Var "U")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Set (Var "U"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" )  "}"  ))  ")" ); end; 





:: deftheorem    defines :::"One-Point_Compactification"::: COMPACT1:def 9 :  (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v1_pre_topc :::"strict"::: )     ($#l1_pre_topc :::"TopStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_compact1 :::"One-Point_Compactification"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")) ")" ))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X")))  ($#k2_xboole_0 :::"\/"::: )   "{"  (Set  "(" (Set (Var "U"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) where U "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "("  (Bool (Set (Var "U")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Set (Var "U"))  ($#k3_subset_1 :::"`"::: )  ) "is"   ($#v2_compts_1 :::"compact"::: )  )  ")" )  "}"  ))  ")" )  ")" ))); 
 registrationlet "X" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster (Set   ($#k1_compact1 :::"One-Point_Compactification"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: COMPACT1:4 (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_compact1 :::"One-Point_Compactification"::: )  (Set (Var "X")) ")" )))) ; 
 registrationlet "X" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_compact1 :::"One-Point_Compactification"::: )  "X") ->   ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )   ; 
end; 
theorem :: COMPACT1:5 (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set (Var "X")) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k1_compact1 :::"One-Point_Compactification"::: )  (Set (Var "X"))))) ; 
 registrationlet "X" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_compact1 :::"One-Point_Compactification"::: )  "X") ->   ($#v1_pre_topc :::"strict"::: )     ($#v1_compts_1 :::"compact"::: )   ; 
end; 
theorem :: COMPACT1:6 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v8_pre_topc :::"Hausdorff"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v5_compact1 :::"locally-compact"::: )  )  ")" ) "iff" (Bool (Set   ($#k1_compact1 :::"One-Point_Compactification"::: )  (Set (Var "X"))) "is"   ($#v8_pre_topc :::"Hausdorff"::: )  )  ")" )) ; 
 
theorem :: COMPACT1:7 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_compts_1 :::"compact"::: )  )) "iff" (Bool  "ex" (Set (Var "X9")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k1_compact1 :::"One-Point_Compactification"::: )  (Set (Var "X")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "X9"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X")))) & (Bool (Set (Var "X9")) "is"   ($#v1_tops_1 :::"dense"::: )  )  ")" ))  ")" )) ; 
 
theorem :: COMPACT1:8 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_compts_1 :::"compact"::: )  ))) "holds"  (Bool (Set   ($#k1_yellow_9 :::"incl"::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k1_compact1 :::"One-Point_Compactification"::: )  (Set (Var "X")) ")" ) ")" ) "is"   ($#v7_compact1 :::"compactification"::: )  )) ;