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

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 :: thesis: for x, y being Point of Y st 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 ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W )

hence
A is T_0
; :: thesis: verum( not V is open or not x in V or y in V ) ) holds

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: ( 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 that

A2: x in A and

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

{x} c= A by A2, ZFMISC_1:31;

then consider G being Subset of Y such that

A4: G is open and

A5: A /\ G = {x} by A1, TEX_2:def 3;

assume A6: 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 ) )

( 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;( 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 that

A2: x in A and

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

{x} c= A by A2, ZFMISC_1:31;

then consider G being Subset of Y such that

A4: G is open and

A5: A /\ G = {x} by A1, TEX_2:def 3;

assume A6: 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 :: thesis: ex G being Subset of Y st

( G is open & x in G & not y in G )

hence
( ex V being Subset of Y st ( G is open & x in G & not y in G )

take G = G; :: thesis: ( G is open & x in G & not y in G )

thus G is open by A4; :: thesis: ( x in G & not y in G )

x in {x} by TARSKI:def 1;

hence x in G by A5, XBOOLE_0:def 4; :: thesis: not y in G

end;thus G is open by A4; :: thesis: ( x in G & not y in G )

x in {x} by TARSKI:def 1;

hence x in G by A5, XBOOLE_0:def 4; :: thesis: not y in G

now :: thesis: not y in G

hence
not y in G
; :: thesis: verumassume
y in G
; :: thesis: contradiction

then y in {x} by A3, A5, XBOOLE_0:def 4;

hence contradiction by A6, TARSKI:def 1; :: thesis: verum

end;then y in {x} by A3, A5, XBOOLE_0:def 4;

hence contradiction by A6, TARSKI:def 1; :: thesis: verum

( 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