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

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

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

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in {0} ; :: thesis:
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:

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: