set c = Unique_No O;
consider A being Ordinal such that
A1: O == No_Ordinal_op A by Lm24;
Unique_No O == O by SURREALO:def 10;
then A2: Unique_No O == No_Ordinal_op A by A1, SURREALO:4;
then A3: ( born (Unique_No O) = born_eq (Unique_No O) & born_eq (Unique_No O) c= born (No_Ordinal_op A) & born (No_Ordinal_op A) = A ) by SURREALO:def 5, SURREALO:48, Th70;
assume not Unique_No O is No_ordinal ; :: thesis: contradiction
then consider C being object such that
A4: C in R_ (Unique_No O) by XBOOLE_0:def 1;
reconsider C = C as Surreal by A4, SURREAL0:def 16;
C in (L_ (Unique_No O)) \/ (R_ (Unique_No O)) by A4, XBOOLE_0:def 3;
then A5: born C in born (Unique_No O) by SURREALO:1;
C in Day (born C) by SURREAL0:def 18;
then C <= No_Ordinal_op (born C) by Th69;
then C < No_Ordinal_op A by A5, Th68, A3, SURREALO:4;
then A6: C <= Unique_No O by A2, SURREALO:4;
( Unique_No O in {(Unique_No O)} & {(Unique_No O)} << R_ (Unique_No O) ) by TARSKI:def 1, SURREALO:11;
hence contradiction by A4, A6; :: thesis: verum