set S = Sierpinski_Space ;
let p be Point of Sierpinski_Space ; :: thesis: ( p = 0 implies {p} is closed )
A1: the carrier of Sierpinski_Space = {0 ,1} by WAYBEL18:def 9;
assume A2: p = 0 ; :: thesis: {p} is closed
A3: ([#] Sierpinski_Space ) \ {p} = {1}

proof

thus ([#] Sierpinski_Space ) \ {p} c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= ([#] Sierpinski_Space ) \ {p}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ([#] Sierpinski_Space ) \ {p} or a in {1} )
assume A4: a in ([#] Sierpinski_Space ) \ {p} ; :: thesis: a in {1}
then not a in {p} by XBOOLE_0:def 5;
then a <> 0 by A2, TARSKI:def 1;
then a = 1 by A1, A4, TARSKI:def 2;
hence a in {1} by TARSKI:def 1; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {1} or a in ([#] Sierpinski_Space ) \ {p} )
assume a in {1} ; :: thesis: a in ([#] Sierpinski_Space ) \ {p}
then A5: a = 1 by TARSKI:def 1;
then A6: not a in {p} by A2, TARSKI:def 1;
a in [#] Sierpinski_Space by A1, A5, TARSKI:def 2;
hence a in ([#] Sierpinski_Space ) \ {p} by A6, XBOOLE_0:def 5; :: thesis: verum

end;

the topology of Sierpinski_Space = {{} ,{1},{0 ,1}} by WAYBEL18:def 9;
hence ([#] Sierpinski_Space ) \ {p} in the topology of Sierpinski_Space by A3, ENUMSET1:def 1; :: according to PRE_TOPC:def 5,PRE_TOPC:def 6 :: thesis: verum