set c = Unique_No x;
born_eq (Unique_No x) = born_eq x by Def10, Th33;
then Unique_No x in (unique_No_op (born_eq (Unique_No x))) . (born_eq (Unique_No x)) by Def10;
hence Unique_No x is uniq-surreal by Def10; :: thesis: verum