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;
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 b1, b2 being Element of the carrier of T holds
( b1 = b2 or ex b3 being Element of K19( the carrier of T) st
( b3 is open & ( ( b1 in b3 & not b2 in b3 ) or ( b2 in b3 & not b1 in b3 ) ) ) )

let x, y be Point of T; :: thesis: ( x = y or ex b1 being Element of K19( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) )

assume x <> y ; :: thesis: ex b1 being Element of K19( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) )

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 b1 being Element of K19( the carrier of T) st
( b1 is open & ( ( x in b1 & not y in b1 ) or ( y in b1 & not x in b1 ) ) ) ; :: thesis: verum