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

proof

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

proof

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

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {0} or a in ([#] Sierpinski_Space) \ {p} )
assume a in {0} ; :: thesis: a in ([#] Sierpinski_Space) \ {p}
then A5: a = 0 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;

A7: {0} <> {1} by ZFMISC_1:3;
A8: {0} <> {0,1} by ZFMISC_1:5;
the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def 9;
hence not ([#] Sierpinski_Space) \ {p} in the topology of Sierpinski_Space by A7, A8, A3, ENUMSET1:def 1; :: according to PRE_TOPC:def 2,PRE_TOPC:def 3 :: thesis: verum