:: deftheorem defines No_uOrdinal_op SURREALN:def 12 :
for A being Ordinal holds No_uOrdinal_op A = Unique_No (No_Ordinal_op A);