theorem :: SRINGS_4:1

for X1, X2, X3, X4 being set holds
( (X1 /\ X4) \ (X2 \/ X3) misses X1 \ ((X2 \/ X3) \/ X4) & (X1 /\ X4) \ (X2 \/ X3) misses ((X1 /\ X3) /\ X4) \ X2 & X1 \ ((X2 \/ X3) \/ X4) misses ((X1 /\ X3) /\ X4) \ X2 ) by Thm01;