let X be set ; :: thesis: for A, B being Subset-Family of X st ( B = A \ {{}} or A = B \/ {{}} ) holds
UniCl A = UniCl B
let A, B be Subset-Family of X; :: thesis: ( ( B = A \ {{}} or A = B \/ {{}} ) implies UniCl A = UniCl B )
assume A1: ( B = A \ {{}} or A = B \/ {{}} ) ; :: thesis: UniCl A = UniCl B
A2: UniCl A c= UniCl B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl A or x in UniCl B )
assume x in UniCl A ; :: thesis: x in UniCl B
then consider Y being Subset-Family of X such that
A3: Y c= A and
A4: x = union Y by CANTOR_1:def 1;
A5: Y \ {{}} c= B

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in Y \ {{}} or w in B )
assume A6: w in Y \ {{}} ; :: thesis: w in B

per cases ( B = A \ {{}} or A = B \/ {{}} ) by A1;

suppose A7: B = A \ {{}} ; :: thesis: w in B

( w in Y & not w in {{}} ) by A6, XBOOLE_0:def 5;
hence w in B by A3, A7, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A8: A = B \/ {{}} ; :: thesis: w in B

( w in Y & not w in {{}} ) by A6, XBOOLE_0:def 5;
hence w in B by A3, A8, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

reconsider Z = Y \ {{}} as Subset-Family of X ;
Z \/ {{}} = Y \/ {{}} by XBOOLE_1:39;
then union (Z \/ {{}}) = (union Y) \/ (union {{}}) by ZFMISC_1:78
.= (union Y) \/ {} by ZFMISC_1:25
.= union Y ;
then x = (union Z) \/ (union {{}}) by A4, ZFMISC_1:78
.= (union Z) \/ {} by ZFMISC_1:25
.= union Z ;
hence x in UniCl B by A5, CANTOR_1:def 1; :: thesis: verum

end;

UniCl B c= UniCl A by A1, CANTOR_1:9, XBOOLE_1:7, XBOOLE_1:36;
hence UniCl A = UniCl B by A2; :: thesis: verum