begin
:: deftheorem Def1 defines SubSpace TSP_1:def 1 :
theorem
canceled;
theorem Th2:
:: deftheorem Def2 defines SubSpace TSP_1:def 2 :
theorem
canceled;
theorem Th4:
begin
:: deftheorem Def3 defines T_0 TSP_1:def 3 :
:: deftheorem Def4 defines T_0 TSP_1:def 4 :
Lm1:
for X being non empty non trivial anti-discrete TopStruct holds not X is T_0
Lm2:
for X being non empty TopSpace
for x being Point of X holds x in Cl {x}
:: deftheorem Def5 defines T_0 TSP_1:def 5 :
:: deftheorem Def6 defines T_0 TSP_1:def 6 :
:: deftheorem defines T_0 TSP_1:def 7 :
begin
:: deftheorem Def8 defines T_0 TSP_1:def 8 :
:: deftheorem Def9 defines T_0 TSP_1:def 9 :
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
:: deftheorem Def10 defines T_0 TSP_1:def 10 :
:: deftheorem Def11 defines T_0 TSP_1:def 11 :
:: deftheorem defines T_0 TSP_1:def 12 :
theorem Th13:
theorem
begin
:: deftheorem defines T_0 TSP_1:def 13 :
:: deftheorem Def14 defines T_0 TSP_1:def 14 :
theorem Th15:
theorem
theorem
theorem
theorem
theorem
theorem