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;