for X being non empty anti-discrete TopSpace
for A being Subset of X holds
( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) ) by PCOMPS_1:2, TDLAT_3:19;