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 )

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

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 A2:
x = x0
; :: thesis: {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;then x0 in {x} by A1, Th38;

hence x = x0 by TARSKI:def 1; :: thesis: verum

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