begin
:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
canceled;
theorem
theorem
canceled;
theorem
:: deftheorem PRE_TOPC:def 2 :
canceled;
:: deftheorem PRE_TOPC:def 3 :
canceled;
:: deftheorem PRE_TOPC:def 4 :
canceled;
:: deftheorem Def5 defines open PRE_TOPC:def 5 :
:: deftheorem Def6 defines closed PRE_TOPC:def 6 :
:: deftheorem PRE_TOPC:def 7 :
canceled;
:: deftheorem PRE_TOPC:def 8 :
canceled;
:: deftheorem Def9 defines SubSpace PRE_TOPC:def 9 :
Lm1:
for T being TopStruct holds TopStruct(# the carrier of T,the topology of T #) is SubSpace of T
:: deftheorem Def10 defines | PRE_TOPC:def 10 :
theorem
theorem Th29:
theorem
:: deftheorem PRE_TOPC:def 11 :
canceled;
:: deftheorem Def12 defines continuous PRE_TOPC:def 12 :
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th39:
theorem
canceled;
theorem
theorem
canceled;
theorem Th43:
theorem Th44:
:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem
theorem
theorem Th52:
theorem
theorem
begin
theorem
theorem
theorem
:: deftheorem defines T_0 PRE_TOPC:def 14 :
:: deftheorem Def15 defines T_1 PRE_TOPC:def 15 :
:: deftheorem Def16 defines T_2 PRE_TOPC:def 16 :
:: deftheorem defines regular PRE_TOPC:def 17 :
:: deftheorem defines normal PRE_TOPC:def 18 :
:: deftheorem Def19 defines T_3 PRE_TOPC:def 19 :
:: deftheorem Def20 defines T_4 PRE_TOPC:def 20 :
theorem
theorem
theorem
theorem Th61:
theorem Th62:
theorem Th63:
theorem
theorem Th65:
theorem