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;

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

hence
Y is T_0
; :: thesis: verum( 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;( 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