theorem Th65: :: SURREALN:65

for A being Ordinal holds No_Ordinal_op (succ A) = [{(No_Ordinal_op A)},{}]