theorem Th71: :: SURREALN:71

for A being Ordinal
for x being Surreal st x in L_ (No_Ordinal_op A) holds
ex B being Ordinal st
( B in A & x = No_Ordinal_op B )