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 ) ) )
A1: the carrier of (x0 -PointClTop X) = X by Def7;
assume A2: {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 by XBOOLE_1:62;
reconsider A = {x0} as Subset of Y by A2, XBOOLE_0:def 8;
A3: x0 in A by TARSKI:def 1;
reconsider A = A as proper Subset of Y by A2, SUBSET_1:def 7;

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

assume A4: {x} is open Subset of (x0 -PointClTop X) ; :: thesis: ( x in X & not x = x0 )
hence x in X by A1, ZFMISC_1:37; :: 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 A1, TARSKI:def 1; :: thesis: verum

end;

assume ( x in X & x <> x0 ) ; :: thesis: {x} is open Subset of (x0 -PointClTop X)
then A5: ( not x0 in {x} & x0 in Y & {x} c= X ) by A3, TARSKI:def 1, ZFMISC_1:37;
then {x} is proper Subset of (x0 -PointClTop Y) by A1, SUBSET_1:def 7;
hence {x} is open Subset of (x0 -PointClTop X) by A5, Th39; :: thesis: verum