set S = Sierpinski_Space ;
ex p being Point of Sierpinski_Space st Cl {p} <> {p}
proof
the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def 9;
then reconsider p = 1 as Point of Sierpinski_Space by TARSKI:def 2;
take p ; :: thesis: Cl {p} <> {p}
thus Cl {p} <> {p} by Th2; :: thesis: verum
end;
hence not Sierpinski_Space is T_1 by YELLOW_8:26; :: thesis: verum