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};

thus ( S1 <> {} implies union (B \/ {S1}) <> union B ) :: thesis: verum

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

{S1} c= bool Y
c1 misses c2

let c1, c2 be set ; :: thesis: ( c1 in B \/ {S1} & c2 in B \/ {S1} & c1 <> c2 implies b_{1} misses b_{2} )

assume that

A3: c1 in B \/ {S1} and

A4: c2 in B \/ {S1} and

A5: c1 <> c2 ; :: thesis: b_{1} misses b_{2}

end;assume that

A3: c1 in B \/ {S1} and

A4: c2 in B \/ {S1} and

A5: c1 <> c2 ; :: thesis: b

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

end;

suppose
c1 in {S1}
; :: thesis: b_{1} misses b_{2}

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;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

proof

hence
B \/ {S1} is mutually-disjoint Subset-Family of Y
by A2, Def5, XBOOLE_1:8; :: thesis: ( S1 <> {} implies union (B \/ {S1}) <> union B )
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;assume p in {S1} ; :: thesis: p in bool Y

then p = S1 by TARSKI:def 1;

hence p in bool Y ; :: thesis: verum

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

end;not union (B \/ {S1}) c= union B

proof

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