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 20 :: thesis: ( not l1 in -- Y or not r1 in -- X or not r1 <= l1 )
assume A2: ( l1 in -- Y & r1 in -- X ) ; :: thesis: not r1 <= l1
A3: ex l being Surreal st
( l in Y & l1 = - l ) by A2, Def4;
ex r being Surreal st
( r in X & r1 = - r ) by A2, Def4;
hence not r1 <= l1 by A3, A1, Th10; :: thesis: verum