theorem :: SURREALO:31

for X1, X2, Y1, Y2 being set st X1 <=_ X2 & Y1 <=_ Y2 holds
X1 \/ Y1 <=_ X2 \/ Y2