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= Cl (union F) :: thesis:

let B be Subset of T; :: thesis:
assume B in F ; :: thesis:
then A1: B c= union F by ZFMISC_1:74;
union F c= Cl (union F) by PRE_TOPC:18;
hence B c= Cl (union F) by A1; :: thesis:

end;

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

let A be Subset of T; :: thesis:
reconsider A1 = A as Subset of T ;
assume A is closed_condensed ; :: thesis:
then A2: A1 is closed by TOPS_1:66;
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 union F c= A by ZFMISC_1:76;
then Cl (union F) c= Cl A by PRE_TOPC:19;
hence Cl (union F) c= A by A2, PRE_TOPC:22; :: thesis:

end;