let X1, X2, X3, X4 be set ; :: thesis: (X1 \ X2) \ (X3 \ X4) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)
(X1 \ X2) \ (X3 \ X4) = (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) by Thm02;
hence (X1 \ X2) \ (X3 \ X4) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2) by Thm03; :: thesis: verum