theorem Th73: :: SURREALN:73

for A being Ordinal holds
( No_uOrdinal_op A == No_Ordinal_op A & born (No_uOrdinal_op A) = A )