let X, Y be surreal-membered set ; :: thesis: ( X <<= Y implies -- Y <<= -- X )
assume A1: X <<= Y ; :: thesis: -- Y <<= -- X
let l1, r1 be Surreal; :: according to SURREAL0:def 19 :: thesis: ( not l1 in -- X or not r1 in -- Y or r1 <= l1 )
assume A2: ( l1 in -- X & r1 in -- Y ) ; :: thesis: r1 <= l1
consider l being Surreal such that
A3: ( l in X & l1 = - l ) by A2, Def4;
ex r being Surreal st
( r in Y & r1 = - r ) by A2, Def4;
hence r1 <= l1 by A3, A1, Th10; :: thesis: verum