begin
:: deftheorem Def1 defines compact COMPACT1:def 1 :
:: deftheorem Def2 defines relatively-compact COMPACT1:def 2 :
:: deftheorem Def3 defines liminally-compact COMPACT1:def 3 :
:: deftheorem Def4 defines locally-relatively-compact COMPACT1:def 4 :
:: deftheorem Def5 defines locally-closed/compact COMPACT1:def 5 :
:: deftheorem Def6 defines locally-compact COMPACT1:def 6 :
theorem
theorem Th2:
:: deftheorem defines embedding COMPACT1:def 7 :
theorem Th3:
:: deftheorem Def8 defines compactification COMPACT1:def 8 :
:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def 9 :
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem