let X, x0, x be set ; :: thesis: ( x0 in X implies ( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 ) )
assume A1: x0 in X ; :: thesis: ( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 )

hereby :: thesis: ( x = x0 implies {x} is closed Subset of (x0 -PointClTop X) )

assume {x} is closed Subset of (x0 -PointClTop X) ; :: thesis: x = x0
then x0 in {x} by A1, Th38;
hence x = x0 by TARSKI:def 1; :: thesis: verum

end;

assume x = x0 ; :: thesis: {x} is closed Subset of (x0 -PointClTop X)
then ( x0 in {x} & {x} c= X & the carrier of (x0 -PointClTop X) = X ) by A1, Def7, ZFMISC_1:37;
hence {x} is closed Subset of (x0 -PointClTop X) by Th38; :: thesis: verum