let X1, X2, X3, X4 be set ; :: thesis: (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
set M1 = X1 \ (X2 \/ X3);
set M2 = (X1 /\ X4) \ X2;
set M3 = (X1 /\ X4) \ (X2 \/ X3);
set M4 = X1 \ ((X2 \/ X3) \/ X4);
set M5 = ((X1 /\ X3) /\ X4) \ X2;
set Z = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2);
( X1 \ (X2 \/ X3) c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) & (X1 /\ X4) \ X2 c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) ) by Lm1, Lm2;
then (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) c= ((((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)) \/ ((((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)) by XBOOLE_1:13;
hence (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) c= (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) ; :: according to XBOOLE_0:def 10 :: thesis: (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) c= (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)
( (X1 /\ X4) \ (X2 \/ X3) c= (X1 /\ X4) \ X2 & X1 \ ((X2 \/ X3) \/ X4) c= X1 \ (X2 \/ X3) & ((X1 /\ X3) /\ X4) \ X2 c= (X1 /\ X4) \ X2 ) by XBOOLE_1:7, XBOOLE_1:34, Lm3;
then ( ((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4)) c= ((X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)) \/ ((X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2)) & ((X1 /\ X3) /\ X4) \ X2 c= (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) ) by XBOOLE_1:10, XBOOLE_1:13;
hence (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) c= (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) by XBOOLE_1:13; :: thesis: verum