:: deftheorem defines simplest_up_to SURREALC:def 16 :
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( s,y,r simplest_up_to alpha iff for beta being Ordinal st beta in alpha holds
s,y,r simplest_on_position beta );