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;
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 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;
assume that
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