:: deftheorem defines Day SURREAL0:def 13 :
for A being Ordinal holds Day A = Day ((No_Ord A),A);