let X, Y be set ; :: thesis: ( ( for x being Surreal st x in X holds
ex y being Surreal st
( y in Y & x == y ) ) implies X <=_ Y )
assume A1: for x being Surreal st x in X holds
ex y being Surreal st
( y in Y & x == y ) ; :: thesis: X <=_ Y
let x be Surreal; :: according to SURREALO:def 3 :: thesis: ( not x in X or ex b₁, b₂ being set st
( b₁ in Y & b₂ in Y & b₁ <= x & x <= b₂ ) )
assume x in X ; :: thesis: ex b₁, b₂ being set st
( b₁ in Y & b₂ in Y & b₁ <= x & x <= b₂ )
then ex y being Surreal st
( y in Y & x == y ) by A1;
hence ex b₁, b₂ being set st
( b₁ in Y & b₂ in Y & b₁ <= x & x <= b₂ ) ; :: thesis: verum