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 )
A2: A /\ B c= B by XBOOLE_1:17;
Int (A /\ B) c= A /\ B by TOPS_1:16;
then Int (A /\ B) c= B by A2;
then A3: Cl (Int (A /\ B)) c= Cl B by PRE_TOPC:19;
assume Cl (Int (A /\ B)) = A ; :: thesis: A c= B
hence A c= B by A1, A3, PRE_TOPC:22; :: thesis: verum