let X, x0, x be set ; ( {x0} c< X implies ( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) ) )
assume A1:
{x0} c< X
; ( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) )
then reconsider Y = X as non empty set ;
reconsider A = {x0} as Subset of Y by A1;
A2:
x0 in A
by TARSKI:def 1;
reconsider A = A as proper Subset of Y by A1, SUBSET_1:def 6;
A3:
the carrier of (x0 -PointClTop X) = X
by Def7;
assume that
A5:
x in X
and
A6:
x <> x0
; {x} is open Subset of (x0 -PointClTop X)
A7:
not x0 in {x}
by A6, TARSKI:def 1;
x0 in Y
by A2;
then
{x} is proper Subset of (x0 -PointClTop Y)
by A7, A5, A3, SUBSET_1:def 6, ZFMISC_1:31;
hence
{x} is open Subset of (x0 -PointClTop X)
by A7, A2, Th39; verum