let X1, X2, X3, X4 be set ; :: thesis: ((X1 /\ X3) /\ X4) \ X2 c= (X1 /\ X4) \ X2
(X1 /\ X3) /\ X4 = (X1 /\ X4) /\ X3 by XBOOLE_1:16;
hence ((X1 /\ X3) /\ X4) \ X2 c= (X1 /\ X4) \ X2 by XBOOLE_1:17, XBOOLE_1:33; :: thesis: verum