theorem Th75: :: SURREALN:75

for A, B being Ordinal holds
( No_uOrdinal_op A < No_uOrdinal_op B iff A in B )