theorem Th79: :: SURREALC:79

for x being Surreal
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( x in_meets_terms s,y,r,alpha iff x in_meets_terms s | (succ alpha),y,r,alpha )