let A, A1, A2, B, B1, B2 be non empty set ; :: thesis: ( ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) iff ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) )

hereby :: thesis: ( ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) implies ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) )

assume A2: ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) ; :: thesis: ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) )
( [:A1,B1:] c= [:A,B:] & [:A2,B2:] c= [:A,B:] ) by A2, XBOOLE_1:7;
then A3: ( A1 c= A & B1 c= B & A2 c= A & B2 c= B ) by ZFMISC_1:114;
[:(A1 \/ A2),(B1 \/ B2):] = (([:A1,B1:] \/ [:A1,B2:]) \/ [:A2,B1:]) \/ [:A2,B2:] by ZFMISC_1:98
.= (([:A1,B1:] \/ [:A1,B2:]) \/ [:A2,B2:]) \/ [:A2,B1:] by XBOOLE_1:4
.= ([:A1,B1:] \/ ([:A2,B2:] \/ [:A1,B2:])) \/ [:A2,B1:] by XBOOLE_1:4
.= (([:A1,B1:] \/ [:A2,B2:]) \/ [:A1,B2:]) \/ [:A2,B1:] by XBOOLE_1:4
.= ([:A1,B1:] \/ [:A2,B2:]) \/ ([:A1,B2:] \/ [:A2,B1:]) by XBOOLE_1:4 ;
then A5: [:A1,B1:] \/ [:A2,B2:] c= [:(A1 \/ A2),(B1 \/ B2):] by XBOOLE_1:7;
A6: [:(A1 /\ A2),(B1 /\ B2):] = {} by A2, ZFMISC_1:100;

per cases ( A1 /\ A2 = {} or B1 /\ B2 = {} ) by A6;

suppose A7: A1 /\ A2 = {} ; :: thesis: ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) )

then B7: A1 misses A2 ;

A12: now :: thesis: not B \ B1 <> {}

assume B \ B1 <> {} ; :: thesis: contradiction
then consider y being object such that
A8: y in B \ B1 by XBOOLE_0:def 1;
A9: ( y in B & not y in B1 ) by A8, XBOOLE_0:def 5;
consider x being object such that
A10: x in A1 by XBOOLE_0:def 1;
A11: [x,y] in [:A,B:] by A3, A10, A8, ZFMISC_1:def 2;
not x in A2 by B7, A10, XBOOLE_0:3;
then ( not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] ) by A9, ZFMISC_1:87;
hence contradiction by A11, A2, XBOOLE_0:def 3; :: thesis: verum

end;

now :: thesis: not B \ B2 <> {}

assume B \ B2 <> {} ; :: thesis: contradiction
then consider y being object such that
A14: y in B \ B2 by XBOOLE_0:def 1;
A15: ( y in B & not y in B2 ) by A14, XBOOLE_0:def 5;
consider x being object such that
A16: x in A2 by XBOOLE_0:def 1;
A17: [x,y] in [:A,B:] by A3, A16, A14, ZFMISC_1:def 2;
not x in A1 by B7, A16, XBOOLE_0:3;
then ( not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] ) by A15, ZFMISC_1:87;
hence contradiction by A17, A2, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) by A3, A5, A7, A12, XBOOLE_1:8, XBOOLE_1:37, A2, ZFMISC_1:114; :: thesis: verum

end;

suppose A18: B1 /\ B2 = {} ; :: thesis: ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) )

then B18: B1 misses B2 ;

A19: now :: thesis: not A \ A1 <> {}

assume A \ A1 <> {} ; :: thesis: contradiction
then consider x being object such that
A20: x in A \ A1 by XBOOLE_0:def 1;
A21: ( x in A & not x in A1 ) by A20, XBOOLE_0:def 5;
consider y being object such that
A22: y in B1 by XBOOLE_0:def 1;
A23: [x,y] in [:A,B:] by A3, A22, A20, ZFMISC_1:def 2;
not y in B2 by B18, A22, XBOOLE_0:3;
then ( not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] ) by A21, ZFMISC_1:87;
hence contradiction by A23, A2, XBOOLE_0:def 3; :: thesis: verum

end;

now :: thesis: not A \ A2 <> {}

assume A \ A2 <> {} ; :: thesis: contradiction
then consider x being object such that
A24: x in A \ A2 by XBOOLE_0:def 1;
A25: ( x in A & not x in A2 ) by A24, XBOOLE_0:def 5;
consider y being object such that
A26: y in B2 by XBOOLE_0:def 1;
A27: [x,y] in [:A,B:] by A3, A26, A24, ZFMISC_1:def 2;
not y in B1 by B18, A26, XBOOLE_0:3;
then ( not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] ) by A25, ZFMISC_1:87;
hence contradiction by A27, A2, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) by A3, A5, A18, A19, XBOOLE_1:8, XBOOLE_1:37, A2, ZFMISC_1:114; :: thesis: verum

end;

end;

end;

assume A28: ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) ; :: thesis: ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] )

per cases ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) by A28;

suppose A29: ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) ; :: thesis: ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] )

for z being object holds not z in [:A1,B1:] /\ [:A2,B2:]

proof

let z be object ; :: thesis: not z in [:A1,B1:] /\ [:A2,B2:]
assume z in [:A1,B1:] /\ [:A2,B2:] ; :: thesis: contradiction
then A31: ( z in [:A1,B1:] & z in [:A2,B2:] ) by XBOOLE_0:def 4;
then consider x, y being object such that
A32: ( x in A1 & y in B1 & z = [x,y] ) by ZFMISC_1:84;
( x in A2 & y in B2 ) by A31, A32, ZFMISC_1:87;
hence contradiction by A32, A29, XBOOLE_0:3; :: thesis: verum

end;

hence ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) by A29, ZFMISC_1:97, XBOOLE_0:4; :: thesis: verum

end;

suppose A33: ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ; :: thesis: ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] )

for z being object holds not z in [:A1,B1:] /\ [:A2,B2:]

proof

let z be object ; :: thesis: not z in [:A1,B1:] /\ [:A2,B2:]
assume z in [:A1,B1:] /\ [:A2,B2:] ; :: thesis: contradiction
then A35: ( z in [:A1,B1:] & z in [:A2,B2:] ) by XBOOLE_0:def 4;
then consider x, y being object such that
A36: ( x in A1 & y in B1 & z = [x,y] ) by ZFMISC_1:84;
( x in A2 & y in B2 ) by A35, A36, ZFMISC_1:87;
hence contradiction by A36, A33, XBOOLE_0:3; :: thesis: verum

end;

hence ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) by A33, ZFMISC_1:97, XBOOLE_0:4; :: thesis: verum

end;

end;