theorem Th72: :: SURREALN:72

for n being Nat holds uInt . n = No_Ordinal_op n