let A, B, C, D, X1, X2, X3, X4 be set ; :: thesis: ( 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 AS: ( A /\ B = {} & C c= A & D c= B & X1 c= A \ C & X2 c= B \ D & X3 = C & X4 = D ) ; :: thesis: ( X1 /\ X2 = {} & X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
P1: (A \ C) /\ (B \ D) c= A /\ B by XBOOLE_1:27;
X1 /\ X2 c= (A \ C) /\ (B \ D) by AS, XBOOLE_1:27;
hence X1 /\ X2 = {} by AS, P1; :: thesis: ( X1 /\ X3 = {} & X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
P2: (A \ C) /\ C = (C /\ A) \ C by XBOOLE_1:49;
C /\ A c= C by XBOOLE_1:17;
then (A \ C) /\ C = {} by P2, XBOOLE_1:37;
hence X1 /\ X3 = {} by AS, XBOOLE_1:3, XBOOLE_1:27; :: thesis: ( X1 /\ X4 = {} & X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
(A \ C) /\ D = {} by AS, XBOOLE_1:3, XBOOLE_1:27;
hence X1 /\ X4 = {} by AS, XBOOLE_1:3, XBOOLE_1:27; :: thesis: ( X2 /\ X3 = {} & X2 /\ X4 = {} & X3 /\ X4 = {} )
(B \ D) /\ C = {} by AS, XBOOLE_1:3, XBOOLE_1:27;
hence X2 /\ X3 = {} by AS, XBOOLE_1:3, XBOOLE_1:27; :: thesis: ( X2 /\ X4 = {} & X3 /\ X4 = {} )
P6: (B \ D) /\ D = (B /\ D) \ D by XBOOLE_1:49;
B /\ D c= D by XBOOLE_1:17;
then (B \ D) /\ D = {} by P6, XBOOLE_1:37;
hence X2 /\ X4 = {} by AS, XBOOLE_1:3, XBOOLE_1:27; :: thesis: X3 /\ X4 = {}
thus X3 /\ X4 = {} by AS, XBOOLE_1:3, XBOOLE_1:27; :: thesis: verum