let it1, it2 be Ordinal; ( ex y being Surreal st
( born y = it1 & y == x ) & ( for y being Surreal st y == x holds
it1 c= born y ) & ex y being Surreal st
( born y = it2 & y == x ) & ( for y being Surreal st y == x holds
it2 c= born y ) implies it1 = it2 )
assume that
A3:
( ex y being Surreal st
( born y = it1 & y == x ) & ( for y being Surreal st y == x holds
it1 c= born y ) )
and
A4:
( ex y being Surreal st
( born y = it2 & y == x ) & ( for y being Surreal st y == x holds
it2 c= born y ) )
; it1 = it2
( it1 c= it2 & it2 c= it1 )
by A3, A4;
hence
it1 = it2
by XBOOLE_0:def 10; verum