theorem :: SURREALN:80

for A being Ordinal ex x being No_ordinal Surreal st
( born x = A & No_uOrdinal_op A == x & ( for o being object holds
( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) ) ) )