begin
:: deftheorem COMPTS_1:def 1 :
canceled;
:: deftheorem COMPTS_1:def 2 :
canceled;
:: deftheorem Def3 defines compact COMPTS_1:def 3 :
:: deftheorem COMPTS_1:def 4 :
canceled;
:: deftheorem defines regular COMPTS_1:def 5 :
:: deftheorem defines normal COMPTS_1:def 6 :
:: deftheorem Def7 defines compact COMPTS_1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem
:: deftheorem defines 1TopSp COMPTS_1:def 8 :
theorem Th27:
theorem Th28:
theorem
theorem
begin
theorem Th31:
theorem Th32:
theorem