theorem Thm04: :: SRINGS_4:4

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