let T be TopSpace; :: thesis: for A, B being Subset of T st B is closed & Cl (Int (A /\ B)) = A holds
A c= B
let A, B be Subset of T; :: thesis: ( B is closed & Cl (Int (A /\ B)) = A implies A c= B )
assume A1: B is closed ; :: thesis: ( not Cl (Int (A /\ B)) = A or A c= B )
assume A2: Cl (Int (A /\ B)) = A ; :: thesis: A c= B
( Int (A /\ B) c= A /\ B & A /\ B c= B ) by TOPS_1:44, XBOOLE_1:17;
then Int (A /\ B) c= B by XBOOLE_1:1;
then Cl (Int (A /\ B)) c= Cl B by PRE_TOPC:49;
hence A c= B by A1, A2, PRE_TOPC:52; :: thesis: verum