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 A2: x = x0 ; :: thesis: {x} is closed Subset of (x0 -PointClTop X)
then A3: x0 in {x} by ZFMISC_1:31;
{x} c= X by A2, A1, ZFMISC_1:31;
hence {x} is closed Subset of (x0 -PointClTop X) by A3, Def7, Th38; :: thesis: verum