:: deftheorem defines in_meets_terms SURREALC:def 14 :
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal
for x being Surreal holds
( x in_meets_terms s,y,r,alpha iff for beta being Ordinal
for sb, yb being Surreal st beta in alpha & sb = s . beta & yb = y . beta holds
x is sb,yb,r . beta _term );