let X be set ; :: thesis: for A being Subset-Family of X holds A c= UniCl A
let A be Subset-Family of X; :: thesis: A c= UniCl A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in UniCl A )
assume A1: x in A ; :: thesis: x in UniCl A
then reconsider x' = x as Subset of X ;
reconsider s = {x'} as Subset-Family of X by SUBSET_1:63;
reconsider s = s as Subset-Family of X ;
( s c= A & x = union s ) by A1, ZFMISC_1:31, ZFMISC_1:37;
hence x in UniCl A by Def1; :: thesis: verum