theorem :: SURREALR:34

for X, Y1, Y2 being set holds X ++ (Y1 \/ Y2) = (X ++ Y1) \/ (X ++ Y2) by Th33;