let x, y be Surreal; :: thesis: ( [{x},{y}] is Surreal iff x < y )

hereby :: thesis: ( x < y implies [{x},{y}] is Surreal )

assume [{x},{y}] is Surreal ; :: thesis: x < y
then reconsider xy = [{x},{y}] as Surreal ;
( x in L_ xy & L_ xy << R_ xy & y in {y} ) by SURREAL0:45, TARSKI:def 1;
hence x < y ; :: thesis: verum

end;

assume A1: x < y ; :: thesis: [{x},{y}] is Surreal
consider M being Ordinal such that
A2: for o being object st o in {x} \/ {y} holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
[{x},{y}] in Day M by A2, A1, Th21, SURREAL0:46;
hence [{x},{y}] is Surreal ; :: thesis: verum