theorem Th38: :: SURREALO:38

for A, B being Ordinal
for x being Surreal st x in (unique_No_op A) . B holds
( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) )