theorem :: SURREALN:79

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