:: deftheorem Def10 defines Unique_No SURREALO:def 10 :
for x, b₂ being Surreal holds
( b₂ = Unique_No x iff ( b₂ == x & b₂ in (unique_No_op (born_eq x)) . (born_eq x) ) );