set B = born_eq 0_No;
set C = Unique_No 0_No;
Unique_No 0_No in (unique_No_op (born_eq 0_No)) . (born_eq 0_No) by Def10;
then A1: born (Unique_No 0_No) c= born_eq 0_No by Th38;
( born_eq 0_No c= born 0_No & born 0_No = {} ) by Def5, SURREAL0:37;
then born (Unique_No 0_No) = {} by A1;
hence 0_No = Unique_No 0_No by SURREAL0:37; :: thesis: verum