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

A2: now :: thesis: for c1, c2 being set st c1 in B \/ {S1} & c2 in B \/ {S1} & c1 <> c2 holds
c1 misses c2

let c1, c2 be set ; :: thesis: ( c1 in B \/ {S1} & c2 in B \/ {S1} & c1 <> c2 implies b₁ misses b₂ )
assume that
A3: c1 in B \/ {S1} and
A4: c2 in B \/ {S1} and
A5: c1 <> c2 ; :: thesis: b₁ misses b₂

per cases ( c1 in B or c1 in {S1} ) by A3, XBOOLE_0:def 3;

suppose A6: c1 in B ; :: thesis: b₁ misses b₂

per cases ( c2 in B or c2 in {S1} ) by A4, XBOOLE_0:def 3;

suppose c2 in B ; :: thesis: b₁ misses b₂

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

end;

suppose c2 in {S1} ; :: thesis: b₁ misses b₂

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

end;

end;

end;

suppose c1 in {S1} ; :: thesis: b₁ misses b₂

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: verum

end;

end;

end;

{S1} c= bool Y

proof

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

end;

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

proof

assume A8: S1 <> {} ; :: thesis: union (B \/ {S1}) <> union B
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: contradiction
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: verum

end;

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

end;