let Y be set ; :: thesis:
let S1 be Subset of Y; :: thesis:
let B be mutually-disjoint Subset-Family of Y; :: thesis:
assume A1: for b being set st b in B holds
( S1 misses b & Y <> {} ) ; :: thesis:
set C = B \/ {S1};

A2: now :: thesis:

let c1, c2 be set ; :: thesis:
assume that
A3: c1 in B \/ {S1} and
A4: c2 in B \/ {S1} and
A5: c1 <> c2 ; :: thesis:

per cases by A3, XBOOLE_0:def 3;

suppose A6: c1 in B ; :: thesis:

per cases by A4, XBOOLE_0:def 3;

suppose c2 in B ; :: thesis:

hence c1 misses c2 by A5, A6, Def5; :: thesis:

end;

suppose c2 in {S1} ; :: thesis:

then c2 = S1 by TARSKI:def 1;
hence c1 misses c2 by A1, A6; :: thesis:

end;

end;

end;

suppose c1 in {S1} ; :: thesis:

then A7: c1 = S1 by TARSKI:def 1;
then not c2 in {S1} by A5, TARSKI:def 1;
then c2 in B by A4, XBOOLE_0:def 3;
hence c1 misses c2 by A1, A7; :: thesis:

end;

end;

end;

{S1} c= bool Y

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in {S1} ; :: thesis:
then p = S1 by TARSKI:def 1;
hence p in bool Y ; :: thesis:

end;

hence B \/ {S1} is mutually-disjoint Subset-Family of Y by A2, Def5, XBOOLE_1:8; :: thesis:
thus ( S1 <> {} implies union (B \/ {S1}) <> union B ) :: thesis:

proof

assume A8: S1 <> {} ; :: thesis:
not union (B \/ {S1}) c= union B

proof

A9: {S1} c= B \/ {S1} by XBOOLE_1:7;
assume A10: union (B \/ {S1}) c= union B ; :: thesis:
consider p being object such that
A11: p in S1 by A8, XBOOLE_0:def 1;
S1 in {S1} by TARSKI:def 1;
then p in union (B \/ {S1}) by A11, A9, TARSKI:def 4;
then consider S2 being set such that
A12: p in S2 and
A13: S2 in B by A10, TARSKI:def 4;
S1 misses S2 by A1, A13;
hence contradiction by A11, A12, XBOOLE_0:3; :: thesis:

end;

hence union (B \/ {S1}) <> union B ; :: thesis:

end;