theorem Th60: :: SURREALR:60

for x, y being Surreal
for X, Y1, Y2 being set holds comp (X,x,y,(Y1 \/ Y2)) = (comp (X,x,y,Y1)) \/ (comp (X,x,y,Y2))