theorem Thm03: :: SRINGS_4:3

for X1, X2, X3, X4 being set holds (X1 \ (X2 \/ X3)) \/ ((X1 /\ X4) \ X2) = (((X1 /\ X4) \ (X2 \/ X3)) \/ (X1 \ ((X2 \/ X3) \/ X4))) \/ (((X1 /\ X3) /\ X4) \ X2)