let X be TopSpace; :: thesis:
assume A1: for A being Subset of X
for x being Point of X st A = {x} holds
Cl A = the carrier of X ; :: thesis:
for B being Subset of X holds
( not B is closed or B = {} or B = the carrier of X )

let B be Subset of X; :: thesis:
assume A2: B is closed ; :: thesis:
set z = the Element of B;
assume A3: B <> {} ; :: thesis:
then reconsider x = the Element of B as Point of X by TARSKI:def 3;
A4: {x} c= B by A3, ZFMISC_1:31;
then reconsider A = {x} as Subset of X by XBOOLE_1:1;
Cl A = the carrier of X by A1;
then the carrier of X c= B by A2, A4, TOPS_1:5;
hence B = the carrier of X ; :: thesis:

end;