set S = Sierpinski_Space ;
for x, y being Point of Sierpinski_Space st x <> y holds
ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )

proof

set V = {1};
let x, y be Point of Sierpinski_Space; :: thesis: ( x <> y implies ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) )
y in the carrier of Sierpinski_Space ;
then A1: y in {0,1} by Def9;
{1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
x in the carrier of Sierpinski_Space ;
then x in {0,1} by Def9;
then A2: ( x = 0 or x = 1 ) by TARSKI:def 2;
{1} in {{},{1},{0,1}} by ENUMSET1:def 1;
then {1} in the topology of Sierpinski_Space by Def9;
then A3: V is open ;
assume A4: x <> y ; :: thesis: ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )

per cases ( ( x = 0 & y = 1 ) or ( x = 1 & y = 0 ) ) by A4, A1, A2, TARSKI:def 2;

suppose ( x = 0 & y = 1 ) ; :: thesis: ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )

then ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by TARSKI:def 1;
hence ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by A3; :: thesis: verum

end;

suppose ( x = 1 & y = 0 ) ; :: thesis: ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )

then ( ( x in V & not y in V ) or ( y in V & not x in V ) ) by TARSKI:def 1;
hence ex V being Subset of Sierpinski_Space st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) by A3; :: thesis: verum

end;

end;

end;

hence Sierpinski_Space is T_0 ; :: thesis: verum