let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( 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 ) )
let F be Subset-Family of T; :: thesis: ( ( for B being Subset of T st B in F holds
B c= Cl (union F) ) & ( 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 ) )
thus for B being Subset of T st B in F holds
B c= Cl (union F) :: thesis: 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

proof

let B be Subset of T; :: thesis: ( B in F implies B c= Cl (union F) )
assume B in F ; :: thesis: B c= Cl (union F)
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: verum

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: verum

proof

let A be Subset of T; :: thesis: ( A is closed_condensed & ( for B being Subset of T st B in F holds
B c= A ) implies Cl (union F) c= A )
reconsider A1 = A as Subset of T ;
assume A is closed_condensed ; :: thesis: ( ex B being Subset of T st
( B in F & not B c= A ) or Cl (union F) c= A )
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: Cl (union F) c= A
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: verum

end;