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

end;

let a be set ; :: 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 a = 0 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 not ([#] Sierpinski_Space ) \ {p} in the topology of Sierpinski_Space by A3, A4, ENUMSET1:def 1; :: according to PRE_TOPC:def 5,PRE_TOPC:def 6 :: thesis: verum