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 b1 misses b2 )
assume that
A3: c1 in B \/ {S1} and
A4: c2 in B \/ {S1} and
A5: c1 <> c2 ; :: thesis: b1 misses b2
per cases ( c1 in B or c1 in {S1} ) by ;
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 ; :: 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 ;
S1 in {S1} by TARSKI:def 1;
then p in union (B \/ {S1}) by ;
then consider S2 being set such that
A12: p in S2 and
A13: S2 in B by ;
S1 misses S2 by ;
hence contradiction by A11, A12, XBOOLE_0:3; :: thesis: verum
end;
hence union (B \/ {S1}) <> union B ; :: thesis: verum
end;