begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
begin
:: deftheorem Def1 defines discrete TDLAT_3:def 1 :
:: deftheorem Def2 defines anti-discrete TDLAT_3:def 2 :
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem
:: deftheorem Def3 defines almost_discrete TDLAT_3:def 3 :
begin
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def4 defines extremally_disconnected TDLAT_3:def 4 :
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
:: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def 5 :
theorem Th39:
theorem
begin
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem
theorem
theorem Th51:
theorem
theorem
theorem
theorem