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