let T be non empty TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:
thus for B being Subset of T st B in F holds
(meet F) /\ (Cl (Int (meet F))) c= B :: thesis:

proof

let B be Subset of T; :: thesis:
assume B in F ; :: thesis:
then ( (meet F) /\ (Cl (Int (meet F))) c= meet F & meet F c= B ) by SETFAM_1:4, XBOOLE_1:17;
hence (meet F) /\ (Cl (Int (meet F))) c= B by XBOOLE_1:1; :: thesis:

end;

thus ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= (meet F) /\ (Cl (Int (meet F))) ) :: thesis:

proof

assume A1: F <> {} ; :: thesis:
let A be Subset of T; :: thesis:
assume A2: A is condensed ; :: thesis:
assume for B being Subset of T st B in F holds
A c= B ; :: thesis:
then for P being set st P in F holds
A c= P ;
then A3: A c= meet F by A1, SETFAM_1:6;
then Int A c= Int (meet F) by TOPS_1:48;
then ( A c= Cl (Int A) & Cl (Int A) c= Cl (Int (meet F)) ) by A2, PRE_TOPC:49, TOPS_1:def 6;
then A c= Cl (Int (meet F)) by XBOOLE_1:1;
hence A c= (meet F) /\ (Cl (Int (meet F))) by A3, XBOOLE_1:19; :: thesis:

end;