defpred S₁[ Ordinal] means ex y being Surreal st
( born y = $1 & y == x );
S₁[ born x] ;
then A1: ex O being Ordinal st S₁[O] ;
consider A being Ordinal such that
A2: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A1);
take A ; :: thesis: ( ex y being Surreal st
( born y = A & y == x ) & ( for y being Surreal st y == x holds
A c= born y ) )
thus ex y being Surreal st
( born y = A & y == x ) by A2; :: thesis: for y being Surreal st y == x holds
A c= born y
let y be Surreal; :: thesis: ( y == x implies A c= born y )
assume y == x ; :: thesis: A c= born y
hence A c= born y by A2; :: thesis: verum