let Y be non empty TopStruct ; :: thesis: ( Y is trivial implies Y is T_0 )
assume Y is trivial ; :: thesis: Y is T_0
then consider a being Point of Y such that
A1: the carrier of Y = {a} by TEX_1:def 1;

now :: thesis: for x, y being Point of Y holds
( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )

let x, y be Point of Y; :: thesis: ( not x <> y or ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A2: x <> y ; :: thesis: ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) )
x = a by A1, TARSKI:def 1;
hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A1, A2, TARSKI:def 1; :: thesis: verum

end;

hence Y is T_0 ; :: thesis: verum