let A, B, C, D, X1, X2, X3, X4 be set ; ( A /\ B = {} & C c= A & D c= B & X1 c= A \ C & X2 c= B \ D & X3 = C & X4 = D implies ( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} ) )
assume that
A1:
A /\ B = {}
and
A2:
C c= A
and
A3:
D c= B
and
A4:
X1 c= A \ C
and
A5:
X2 c= B \ D
and
A6:
X3 = C
and
A7:
X4 = D
; ( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
A8:
(A \ C) /\ (B \ D) c= A /\ B
by XBOOLE_1:27;
X1 /\ X2 c= (A \ C) /\ (B \ D)
by A4, A5, XBOOLE_1:27;
hence
X1 /\ X2 = {}
by A1, A8; ( X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
A9:
C /\ A c= C
by XBOOLE_1:17;
(A \ C) /\ C = (C /\ A) \ C
by XBOOLE_1:49;
then
(A \ C) /\ C = {}
by A9, XBOOLE_1:37;
hence
X1 /\ X3 = {}
by A4, A6, XBOOLE_1:3, XBOOLE_1:27; ( X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
(A \ C) /\ D = {}
by A1, A3, XBOOLE_1:3, XBOOLE_1:27;
hence
X1 /\ X4 = {}
by A4, A7, XBOOLE_1:3, XBOOLE_1:27; ( X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
(B \ D) /\ C = {}
by A1, A2, XBOOLE_1:3, XBOOLE_1:27;
hence
X2 /\ X3 = {}
by A5, A6, XBOOLE_1:3, XBOOLE_1:27; ( X2 /\ X4 = {} & X3 /\ X4 = {} )
A10:
B /\ D c= D
by XBOOLE_1:17;
(B \ D) /\ D = (B /\ D) \ D
by XBOOLE_1:49;
then
(B \ D) /\ D = {}
by A10, XBOOLE_1:37;
hence
X2 /\ X4 = {}
by A5, A7, XBOOLE_1:3, XBOOLE_1:27; X3 /\ X4 = {}
thus
X3 /\ X4 = {}
by A1, A2, A3, A6, A7, XBOOLE_1:3, XBOOLE_1:27; verum