consider x being Surreal such that
A3: P₁[x] by A1;
set c = Unique_No x;
A4: Unique_No x == x by SURREALO:def 10;
defpred S₁[ Ordinal] means ex y being uSurreal st
( born y = $1 & P₁[y] );
S₁[ born (Unique_No x)] by A4, A3, A2;
then A5: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A6: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A5);
consider s being uSurreal such that
A7: ( born s = A & P₁[s] ) by A6;
take s ; :: thesis: ( P₁[s] & ( for x being uSurreal st P₁[x] & x <> s holds
born s in born x ) )
thus P₁[s] by A7; :: thesis: for x being uSurreal st P₁[x] & x <> s holds
born s in born x
let y be uSurreal; :: thesis: ( P₁[y] & y <> s implies born s in born y )
assume A8: ( P₁[y] & y <> s & not born s in born y ) ; :: thesis: contradiction
( born s c= born y & born y c= born s ) by A8, ORDINAL1:16, A7, A6;
then A9: born s = born y by XBOOLE_0:def 10;
not y == s by A8, SURREALO:50;

per cases then ( y < s or s < y ) ;

suppose y < s ; :: thesis: contradiction

per cases then ( ex xR being Surreal st
( xR in R_ y & y < xR & xR <= s ) or ex yL being Surreal st
( yL in L_ s & y <= yL & yL < s ) ) by SURREALO:13;

suppose ex xR being Surreal st
( xR in R_ y & y < xR & xR <= s ) ; :: thesis: contradiction

then consider xR being Surreal such that
A10: ( xR in R_ y & y < xR & xR <= s ) ;
xR in (L_ y) \/ (R_ y) by A10, XBOOLE_0:def 3;
then A11: born xR in born y by SURREALO:1;
A12: Unique_No xR == xR by SURREALO:def 10;
then ( y <= Unique_No xR & Unique_No xR <= s ) by A10, SURREALO:4;
then A13: A c= born (Unique_No xR) by A6, A8, A2, A7;
born (Unique_No xR) = born_eq (Unique_No xR) by SURREALO:48;
hence contradiction by A11, A7, A9, ORDINAL1:5, A13, A12, SURREALO:def 5; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in L_ s & y <= yL & yL < s ) ; :: thesis: contradiction

then consider yL being Surreal such that
A14: ( yL in L_ s & y <= yL & yL < s ) ;
yL in (L_ s) \/ (R_ s) by A14, XBOOLE_0:def 3;
then A15: born yL in born s by SURREALO:1;
A16: Unique_No yL == yL by SURREALO:def 10;
then ( y <= Unique_No yL & Unique_No yL <= s ) by A14, SURREALO:4;
then A17: A c= born (Unique_No yL) by A6, A8, A2, A7;
born (Unique_No yL) = born_eq (Unique_No yL) by SURREALO:48;
hence contradiction by A15, A7, ORDINAL1:5, A17, A16, SURREALO:def 5; :: thesis: verum

end;

end;

end;

suppose s < y ; :: thesis: contradiction

per cases then ( ex xR being Surreal st
( xR in R_ s & s < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & s <= yL & yL < y ) ) by SURREALO:13;

suppose ex xR being Surreal st
( xR in R_ s & s < xR & xR <= y ) ; :: thesis: contradiction

then consider xR being Surreal such that
A18: ( xR in R_ s & s < xR & xR <= y ) ;
xR in (L_ s) \/ (R_ s) by A18, XBOOLE_0:def 3;
then A19: born xR in born s by SURREALO:1;
A20: Unique_No xR == xR by SURREALO:def 10;
then ( s <= Unique_No xR & Unique_No xR <= y ) by A18, SURREALO:4;
then A21: A c= born (Unique_No xR) by A6, A8, A2, A7;
born (Unique_No xR) = born_eq (Unique_No xR) by SURREALO:48;
hence contradiction by A19, A7, ORDINAL1:5, A21, A20, SURREALO:def 5; :: thesis: verum

end;

suppose ex yL being Surreal st
( yL in L_ y & s <= yL & yL < y ) ; :: thesis: contradiction

then consider yL being Surreal such that
A22: ( yL in L_ y & s <= yL & yL < y ) ;
yL in (L_ y) \/ (R_ y) by A22, XBOOLE_0:def 3;
then A23: born yL in born y by SURREALO:1;
A24: Unique_No yL == yL by SURREALO:def 10;
then ( s <= Unique_No yL & Unique_No yL <= y ) by A22, SURREALO:4;
then A25: A c= born (Unique_No yL) by A6, A8, A2, A7;
born (Unique_No yL) = born_eq (Unique_No yL) by SURREALO:48;
hence contradiction by A23, A7, A9, ORDINAL1:5, A25, A24, SURREALO:def 5; :: thesis: verum

end;

end;

end;

end;