theorem Th37: :: SURREALO:37

for A, B being Ordinal st A c= B holds
(unique_No_op B) | (succ A) = unique_No_op A