let T be non empty TopSpace; :: thesis: for A, B being Subset of T st B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )
let A, B be Subset of T; :: thesis: ( B is condensed implies ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B ) )
assume A1: B is condensed ; :: thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B )
thus ( (Int (Cl (A \/ B))) \/ (A \/ B) = B implies A c= B ) :: thesis: ( A c= B implies (Int (Cl (A \/ B))) \/ (A \/ B) = B )
proof
assume (Int (Cl (A \/ B))) \/ (A \/ B) = B ; :: thesis: A c= B
then A2: A \/ B c= B by XBOOLE_1:7;
A c= A \/ B by XBOOLE_1:7;
hence A c= B by A2; :: thesis: verum
end;
thus ( A c= B implies (Int (Cl (A \/ B))) \/ (A \/ B) = B ) :: thesis: verum
proof
assume A c= B ; :: thesis: (Int (Cl (A \/ B))) \/ (A \/ B) = B
then A3: A \/ B = B by XBOOLE_1:12;
then Int (Cl (A \/ B)) c= B by A1, TOPS_1:def 6;
hence (Int (Cl (A \/ B))) \/ (A \/ B) = B by A3, XBOOLE_1:12; :: thesis: verum
end;