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 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 ) ) ) 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;( 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

( 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

( b

let x, y be Point of T; :: thesis: ( x = y or ex b

( b

assume x <> y ; :: thesis: ex b

( 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

( b