set S = Sierpinski_Space ;
let p be Point of Sierpinski_Space ; :: thesis: ( p = 0 implies {p} is closed )
assume A1: p = 0 ; :: thesis: {p} is closed
A2: the carrier of Sierpinski_Space = {0 ,1} by WAYBEL18:def 9;
A3: the topology of Sierpinski_Space = {{} ,{1},{0 ,1}} by WAYBEL18:def 9;
([#] 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 a in ([#] Sierpinski_Space ) \ {p} ; :: thesis: a in {1}
then ( a in [#] Sierpinski_Space & not a in {p} ) by XBOOLE_0:def 5;
then ( a in the carrier of Sierpinski_Space & a <> 0 ) by A1, TARSKI:def 1;
then a = 1 by A2, 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 a = 1 by TARSKI:def 1;
then ( a in [#] Sierpinski_Space & not a in {p} ) by A1, A2, TARSKI:def 1, TARSKI:def 2;
hence a in ([#] Sierpinski_Space ) \ {p} by XBOOLE_0:def 5; :: thesis: verum

end;

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