let X be set ; :: thesis: for A being empty Subset-Family of X holds UniCl A = {{} }
let A be empty Subset-Family of X; :: thesis: UniCl A = {{} }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {{} } c= UniCl A

let x be set ; :: thesis: ( x in UniCl A implies x in {{} } )
assume x in UniCl A ; :: thesis: x in {{} }
then consider B being Subset-Family of X such that
A1: ( B c= A & x = union B ) by CANTOR_1:def 1;
B = {} by A1;
hence x in {{} } by A1, TARSKI:def 1, ZFMISC_1:2; :: thesis: verum

end;

consider B being empty Subset-Family of X;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in UniCl A )
assume x in {{} } ; :: thesis: x in UniCl A
then ( x = {} & B c= A & union B = {} ) by TARSKI:def 1, ZFMISC_1:2;
hence x in UniCl A by CANTOR_1:def 1; :: thesis: verum