hereby :: thesis: ( ( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ) implies T is T_0 )

assume A1: T is T_0 ; :: thesis: ( not T is empty implies for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) )
assume A2: not T is empty ; :: thesis: for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) )
let x, y be Point of T; :: thesis: ( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) )
assume x <> y ; :: thesis: ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) )
then 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, A2, T_0TOPSP:def 7;
hence ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ; :: thesis: verum

end;

assume A3: ( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) ) ; :: thesis: T is T_0
assume A4: not T is empty ; :: according to T_0TOPSP:def 7 :: thesis: for b₁, b₂ being Element of the carrier of T holds
( b₁ = b₂ or ex b₃ being Element of K21(the carrier of T) st
( b₃ is open & ( ( b₁ in b₃ & not b₂ in b₃ ) or ( b₂ in b₃ & not b₁ in b₃ ) ) ) )
let x, y be Point of T; :: thesis: ( x = y or ex b₁ being Element of K21(the carrier of T) st
( b₁ is open & ( ( x in b₁ & not y in b₁ ) or ( y in b₁ & not x in b₁ ) ) ) )
assume x <> y ; :: thesis: ex b₁ being Element of K21(the carrier of T) st
( b₁ is open & ( ( x in b₁ & not y in b₁ ) or ( y in b₁ & not x in b₁ ) ) )
then ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) by A3, A4;
hence ex b₁ being Element of K21(the carrier of T) st
( b₁ is open & ( ( x in b₁ & not y in b₁ ) or ( y in b₁ & not x in b₁ ) ) ) ; :: thesis: verum