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