let X, Y be set ; :: thesis: for F being a_partition of X
for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
let F be a_partition of X; :: thesis: for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
let G be a_partition of Y; :: thesis: ( X misses Y implies F \/ G is a_partition of X \/ Y )
assume A1: X misses Y ; :: thesis: F \/ G is a_partition of X \/ Y
set PR = F \/ G;
set XY = X \/ Y;
A2: F \/ G is Subset-Family of (X \/ Y) by Th2;
A3: union (F \/ G) = (union F) \/ (union G) by ZFMISC_1:78
.= X \/ (union G) by EQREL_1:def 4
.= X \/ Y by EQREL_1:def 4 ;
now :: thesis: for A being Subset of (X \/ Y) st A in F \/ G holds
( A <> {} & ( for B being Subset of (X \/ Y) holds
( not B in F \/ G or A = B or A misses B ) ) )
let A be Subset of (X \/ Y); :: thesis: ( A in F \/ G implies ( A <> {} & ( for B being Subset of (X \/ Y) holds
( not B in F \/ G or b2 = b3 or b2 misses b3 ) ) ) )
assume A4: A in F \/ G ; :: thesis: ( A <> {} & ( for B being Subset of (X \/ Y) holds
( not B in F \/ G or b2 = b3 or b2 misses b3 ) ) )
( A in F or A in G ) by A4, XBOOLE_0:def 3;
hence A <> {} ; :: thesis: for B being Subset of (X \/ Y) holds
( not B in F \/ G or b2 = b3 or b2 misses b3 )
let B be Subset of (X \/ Y); :: thesis: ( not B in F \/ G or b1 = b2 or b1 misses b2 )
assume A5: B in F \/ G ; :: thesis: ( b1 = b2 or b1 misses b2 )
per cases ( ( A in F & B in F ) or ( A in G & B in G ) or ( A in F & B in G ) or ( A in G & B in F ) ) by A4, A5, XBOOLE_0:def 3;
suppose ( ( A in F & B in F ) or ( A in G & B in G ) ) ; :: thesis: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by EQREL_1:def 4; :: thesis: verum
end;
suppose ( ( A in F & B in G ) or ( A in G & B in F ) ) ; :: thesis: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by A1, XBOOLE_1:64; :: thesis: verum
end;
end;
end;
hence F \/ G is a_partition of X \/ Y by A2, A3, EQREL_1:def 4; :: thesis: verum