let X be TopSpace; :: thesis: for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds
Cl (Int A) = the carrier of X
let A be Subset of X; :: thesis: ( A \/ (Cl (Int A)) = the carrier of X implies Cl (Int A) = the carrier of X )
assume A \/ (Cl (Int A)) = the carrier of X ; :: thesis: Cl (Int A) = the carrier of X
then ( (Int A) \/ (Cl (Int A)) = the carrier of X & Int A c= Cl (Int A) ) by PRE_TOPC:48, TDLAT_3:6;
hence Cl (Int A) = the carrier of X by XBOOLE_1:12; :: thesis: verum