let X, x0, x be set ; :: thesis: ( {x0} c< X implies ( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) ) )

assume A1: {x0} c< X ; :: thesis: ( {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;

A5: x in X and

A6: x <> x0 ; :: thesis: {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; :: thesis: verum

assume A1: {x0} c< X ; :: thesis: ( {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;

hereby :: thesis: ( x in X & x <> x0 implies {x} is open Subset of (x0 -PointClTop X) )

assume that assume A4:
{x} is open Subset of (x0 -PointClTop X)
; :: thesis: ( x in X & not x = x0 )

hence x in X by A3, ZFMISC_1:31; :: thesis: not x = x0

assume x = x0 ; :: thesis: contradiction

then ( not x0 in {x0} or A is non proper Subset of (x0 -PointClTop X) ) by A4, Th39;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;hence x in X by A3, ZFMISC_1:31; :: thesis: not x = x0

assume x = x0 ; :: thesis: contradiction

then ( not x0 in {x0} or A is non proper Subset of (x0 -PointClTop X) ) by A4, Th39;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

A5: x in X and

A6: x <> x0 ; :: thesis: {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; :: thesis: verum