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 by TDLAT_3:4;
hence Cl (Int A) = the carrier of X by PRE_TOPC:18, XBOOLE_1:12; :: thesis: verum