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
B c= (union F) \/ (Int (Cl (union F))) :: thesis:

proof

let B be Subset of T; :: thesis:
assume B in F ; :: thesis:
then ( B c= union F & union F c= (union F) \/ (Int (Cl (union F))) ) by XBOOLE_1:7, ZFMISC_1:92;
hence B c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:1; :: thesis:

end;

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

proof

let A be Subset of T; :: thesis:
assume A1: A is condensed ; :: thesis:
assume for B being Subset of T st B in F holds
B c= A ; :: thesis:
then for P being set st P in F holds
P c= A ;
then A2: union F c= A by ZFMISC_1:94;
then Cl (union F) c= Cl A by PRE_TOPC:49;
then ( Int (Cl (union F)) c= Int (Cl A) & Int (Cl A) c= A ) by A1, TOPS_1:48, TOPS_1:def 6;
then Int (Cl (union F)) c= A by XBOOLE_1:1;
hence (union F) \/ (Int (Cl (union F))) c= A by A2, XBOOLE_1:8; :: thesis:

end;