let X1, X2, Y be set ; :: thesis: ( X1 << Y & X2 << Y implies X1 \/ X2 << Y )
assume A1: ( X1 << Y & X2 << Y ) ; :: thesis: X1 \/ X2 << Y
let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( l in X1 \/ X2 & r in Y implies not r <= l )
assume A2: ( l in X1 \/ X2 & r in Y ) ; :: thesis: not r <= l
( l in X1 or l in X2 ) by A2, XBOOLE_0:def 3;
hence not r <= l by A1, A2; :: thesis: verum