let Y be non empty TopStruct ; :: thesis: for A being Subset of Y st A is discrete holds
A is T_0
let A be Subset of Y; :: thesis: ( A is discrete implies A is T_0 )
assume A1: A is discrete ; :: thesis: A is T_0

now

let x, y be Point of Y; :: thesis: ( x in A & y in A & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) implies ex W being Subset of Y st
( W is open & not x in W & y in W ) )
assume A2: ( x in A & y in A ) ; :: 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 ) )
then {x} c= A by ZFMISC_1:37;
then consider G being Subset of Y such that
A3: G is open and
A4: A /\ G = {x} by A1, TEX_2:def 5;
assume A5: 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 G = G; :: thesis: ( G is open & x in G & not y in G )
thus G is open by A3; :: thesis: ( x in G & not y in G )
x in {x} by TARSKI:def 1;
hence x in G by A4, XBOOLE_0:def 4; :: thesis: not y in G

now

assume y in G ; :: thesis: contradiction
then y in {x} by A2, A4, XBOOLE_0:def 4;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

hence not y in G ; :: 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 A is T_0 by Def8; :: thesis: verum