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