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 object ; :: 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 and
A2: x = union B by CANTOR_1:def 1;
B = {} by A1;
hence x in {{}} by A2, TARSKI:def 1, ZFMISC_1:2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{}} or x in UniCl A )
assume x in {{}} ; :: thesis: x in UniCl A
then A3: x = {} by TARSKI:def 1;
union ({} (bool X)) = {} by ZFMISC_1:2;
hence x in UniCl A by A3, CANTOR_1:def 1; :: thesis: verum