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

now :: thesis:

let x, y be Point of Y; :: thesis:
assume A2: x <> y ; :: thesis:
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:

end;

hence Y is T_0 ; :: thesis: