begin
theorem
canceled;
theorem Th2:
:: deftheorem defines are_homeomorphic T_0TOPSP:def 1 :
:: deftheorem Def2 defines open T_0TOPSP:def 2 :
:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :
:: deftheorem defines Indiscernible T_0TOPSP:def 4 :
:: deftheorem defines T_0-reflex T_0TOPSP:def 5 :
:: deftheorem defines T_0-canonical_map T_0TOPSP:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
Lm1:
for T being non empty TopSpace
for x, y being Point of (T_0-reflex T) st x <> y holds
ex V being Subset of (T_0-reflex T) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
:: deftheorem Def7 defines T_0 T_0TOPSP:def 7 :
theorem
theorem
theorem Th15:
theorem Th16:
theorem