theorem Th33: :: SURREALR:33

for X1, X2, Y being set holds (X1 \/ X2) ++ Y = (X1 ++ Y) \/ (X2 ++ Y)