theorem Thm02: :: SRINGS_4:2

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