let T be non empty TopSpace; :: thesis: for A, B being Subset of T st B is open_condensed & A c= B holds
Int (Cl (A \/ B)) = B
let A, B be Subset of T; :: thesis: ( B is open_condensed & A c= B implies Int (Cl (A \/ B)) = B )
assume A1: B is open_condensed ; :: thesis: ( not A c= B or Int (Cl (A \/ B)) = B )
assume A c= B ; :: thesis: Int (Cl (A \/ B)) = B
then A \/ B = B by XBOOLE_1:12;
hence Int (Cl (A \/ B)) = B by A1, TOPS_1:def 8; :: thesis: verum