let X be non empty anti-discrete TopSpace; :: thesis: for A being Subset of X holds
( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) )
let A be Subset of X; :: thesis: ( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) )
thus ( A is empty implies Cl A = {} ) by PRE_TOPC:52; :: thesis: ( not A is empty implies Cl A = the carrier of X )
thus ( not A is empty implies Cl A = the carrier of X ) :: thesis: verum

proof

assume not A is empty ; :: thesis: Cl A = the carrier of X
then Cl A <> {} by PCOMPS_1:2;
hence Cl A = the carrier of X by TDLAT_3:21; :: thesis: verum

end;