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 K19( 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 K19( 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 K19( 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 K19( 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