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
then B c= A by XBOOLE_1:7, XBOOLE_1:36;
then A2: UniCl B c= UniCl A by CANTOR_1:9;
UniCl A c= UniCl B

proof

let x be set ; :: 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 set ; :: 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:96
.= (union Y) \/ {} by ZFMISC_1:31
.= union Y ;
then x = (union Z) \/ (union {{} }) by A4, ZFMISC_1:96
.= (union Z) \/ {} by ZFMISC_1:31
.= union Z ;
hence x in UniCl B by A5, CANTOR_1:def 1; :: thesis: verum

end;

hence UniCl A = UniCl B by A2, XBOOLE_0:def 10; :: thesis: verum