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 object ; :: 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 x9 = x as Subset of X ;
reconsider s = {x9} as Subset-Family of X by SUBSET_1:41;
A2: x = union s by ZFMISC_1:25;
s c= A by A1, ZFMISC_1:31;
hence x in UniCl A by A2, Def1; :: thesis: verum