let x, y be Surreal; :: thesis: ( x == y implies Unique_No x = Unique_No y )
assume A1: x == y ; :: thesis: Unique_No x = Unique_No y
then A2: born_eq x = born_eq y by Th33;
Unique_No y == y by Def10;
then ( Unique_No y == x & Unique_No y in (unique_No_op (born_eq x)) . (born_eq x) ) by A2, Def10, A1, Th4;
hence Unique_No x = Unique_No y by Def10; :: thesis: verum