let X be set ; :: thesis: for S being Subset-Family of X
for A, B being Element of S
for p being finite Subset of S st B <> {} & B c= A & p is a_partition of A \ B holds
{B} \/ p is a_partition of A
let S be Subset-Family of X; :: thesis: for A, B being Element of S
for p being finite Subset of S st B <> {} & B c= A & p is a_partition of A \ B holds
{B} \/ p is a_partition of A
let A, B be Element of S; :: thesis: for p being finite Subset of S st B <> {} & B c= A & p is a_partition of A \ B holds
{B} \/ p is a_partition of A
let p be finite Subset of S; :: thesis: ( B <> {} & B c= A & p is a_partition of A \ B implies {B} \/ p is a_partition of A )
assume A1: B <> {} ; :: thesis: ( not B c= A or not p is a_partition of A \ B or {B} \/ p is a_partition of A )
assume A2: B c= A ; :: thesis: ( not p is a_partition of A \ B or {B} \/ p is a_partition of A )
assume A3: p is a_partition of A \ B ; :: thesis: {B} \/ p is a_partition of A
A4: {B} \/ p is Subset-Family of A

proof

A5: p c= bool A

proof

bool (A \ B) c= bool A by ZFMISC_1:67;
hence p c= bool A by A3, XBOOLE_1:1; :: thesis: verum

end;

{B} c= bool A

proof

A6: {B} c= bool B by ZFMISC_1:68;
bool B c= bool A by A2, ZFMISC_1:67;
hence {B} c= bool A by A6, XBOOLE_1:1; :: thesis: verum

end;

hence {B} \/ p is Subset-Family of A by A5, XBOOLE_1:8; :: thesis: verum

end;

A7: union ({B} \/ p) = A

proof

union ({B} \/ p) = (union {B}) \/ (union p) by ZFMISC_1:78
.= B \/ (A \ B) by A3, EQREL_1:def 4
.= A \/ B by XBOOLE_1:39 ;
hence union ({B} \/ p) = A by A2, XBOOLE_1:12; :: thesis: verum

end;

for a being Subset of A st a in {B} \/ p holds
( a <> {} & ( for b being Subset of A holds
( not b in {B} \/ p or a = b or a misses b ) ) )

proof

let a be Subset of A; :: thesis: ( a in {B} \/ p implies ( a <> {} & ( for b being Subset of A holds
( not b in {B} \/ p or a = b or a misses b ) ) ) )
assume A8: a in {B} \/ p ; :: thesis: ( a <> {} & ( for b being Subset of A holds
( not b in {B} \/ p or a = b or a misses b ) ) )
then A9: ( a in {B} or a in p ) by XBOOLE_0:def 3;
thus a <> {} by A1, A3, A8; :: thesis: for b being Subset of A holds
( not b in {B} \/ p or a = b or a misses b )
thus for b being Subset of A holds
( not b in {B} \/ p or a = b or a misses b ) :: thesis: verum

proof

let b be Subset of A; :: thesis: ( not b in {B} \/ p or a = b or a misses b )
assume b in {B} \/ p ; :: thesis: ( a = b or a misses b )
then ( b in {B} or b in p ) by XBOOLE_0:def 3;
then A10: ( ( a = B & b = B ) or ( a = B & b in p ) or ( a in p & b = B ) or ( a in p & b in p ) ) by A9, TARSKI:def 1;
A11: ( a = B & b in p implies a misses b )

proof

assume A12: ( a = B & b in p ) ; :: thesis: a misses b
A \ B misses B by XBOOLE_1:85;
hence a misses b by A3, A12, XBOOLE_1:63; :: thesis: verum

end;

( a in p & b = B implies a misses b )

proof

assume A14: ( a in p & b = B ) ; :: thesis: a misses b
A \ B misses B by XBOOLE_1:85;
hence a misses b by A3, A14, XBOOLE_1:63; :: thesis: verum

end;

hence ( a = b or a misses b ) by A3, A10, A11, EQREL_1:def 4; :: thesis: verum

end;

end;

hence {B} \/ p is a_partition of A by A4, A7, EQREL_1:def 4; :: thesis: verum