let x be Surreal; :: thesis: ( x is uSurreal implies born x = born_eq x )
set B = born_eq x;
assume x is uSurreal ; :: thesis: born x = born_eq x
then x = Unique_No x by Def11;
then x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
hence born x = born_eq x by Th38; :: thesis: verum