thus ( not T is T_0 or T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) by PRE_TOPC:def 8; :: thesis: ( ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) implies T is T_0 )
assume A1: ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) ; :: thesis: T is T_0
let x, y be Point of T; :: according to PRE_TOPC:def 8 :: thesis: ( ex b₁ being Element of K10( the carrier of T) st
( b₁ is open & ( ( x in b₁ & not y in b₁ ) or ( y in b₁ & not x in b₁ ) ) ) or x = y )
assume A2: for G being Subset of T st G is open holds
( x in G iff y in G ) ; :: thesis: x = y

per cases ( T is empty or for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) by A1;

suppose A3: T is empty ; :: thesis: x = y

then x = {} by SUBSET_1:def 1;
hence x = y by A3, SUBSET_1:def 1; :: thesis: verum

end;

suppose for x, y being Point of T st x <> y holds
ex V being Subset of T st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ; :: thesis: x = y

hence x = y by A2; :: thesis: verum

end;

end;