let X be TopSpace; :: thesis: for A, B being Subset of X holds (Int A) /\ (Cl B) c= Cl (A /\ B)
let A, B be Subset of X; :: thesis: (Int A) /\ (Cl B) c= Cl (A /\ B)
(Int A) /\ B c= A /\ B by TOPS_1:16, XBOOLE_1:26;
then A1: Cl ((Int A) /\ B) c= Cl (A /\ B) by PRE_TOPC:19;
(Int A) /\ (Cl B) c= Cl ((Int A) /\ B) by TOPS_1:13;
hence (Int A) /\ (Cl B) c= Cl (A /\ B) by A1, XBOOLE_1:1; :: thesis: verum