let Y be non empty TopSpace; :: thesis: ( Y is discrete implies Y is T_0 )
assume A1: Y is discrete ; :: thesis: Y is T_0

now

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

now

take V = {x}; :: thesis: ( V is open & x in V & not y in V )
thus V is open by A1, TDLAT_3:17; :: thesis: ( x in V & not y in V )
thus x in V by TARSKI:def 1; :: thesis: not y in V
thus not y in V by A2, TARSKI:def 1; :: thesis: verum

end;

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 ) ) ; :: thesis: verum

end;

hence Y is T_0 by Def3; :: thesis: verum