:: deftheorem defines simplest_on_position SURREALC:def 15 :
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( s,y,r simplest_on_position alpha iff for sa being Surreal st sa = s . alpha holds
( ( 0 = alpha implies sa = 0_No ) & ( 0 <> alpha implies ( sa in_meets_terms s,y,r,alpha & ( for x being uSurreal st x in_meets_terms s,y,r,alpha & x <> sa holds
born sa in born x ) ) ) ) );