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

proof

assume A1: F is closed ; :: thesis:
let B be Subset of T; :: thesis:
assume B in F ; :: thesis:
then A2: meet F c= B by SETFAM_1:4;
( Int (meet F) c= meet F & meet F is closed ) by A1, TOPS_1:44, TOPS_2:29;
then ( Cl (Int (meet F)) c= Cl (meet F) & Cl (meet F) = meet F ) by PRE_TOPC:49, PRE_TOPC:52;
hence Cl (Int (meet F)) c= B by A2, XBOOLE_1:1; :: thesis:

end;

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

proof

assume A3: F <> {} ; :: thesis:
let A be Subset of T; :: thesis:
assume A4: A is closed_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 A c= meet F by A3, SETFAM_1:6;
then Int A c= Int (meet F) by TOPS_1:48;
then ( A = Cl (Int A) & Cl (Int A) c= Cl (Int (meet F)) ) by A4, PRE_TOPC:49, TOPS_1:def 7;
hence A c= Cl (Int (meet F)) ; :: thesis:

end;