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