let T be TopSpace; :: thesis: for F being Subset-Family of T holds union (Cl F) c= Cl (union F)
let F be Subset-Family of T; :: thesis: union (Cl F) c= Cl (union F)
for A being set st A in Cl F holds
A c= Cl (union F)

proof

let A be set ; :: thesis: ( A in Cl F implies A c= Cl (union F) )
assume A1: A in Cl F ; :: thesis: A c= Cl (union F)
then reconsider A0 = A as Subset of T ;
ex B being Subset of T st
( A0 = Cl B & B in F ) by A1, PCOMPS_1:def 2;
hence A c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74; :: thesis: verum

end;

hence union (Cl F) c= Cl (union F) by ZFMISC_1:76; :: thesis: verum