theorem Th83: :: SURREALC:83

for x being Surreal
for r being Sequence of REAL
for y, s being Sequence
for A, B being Ordinal st A c= B holds
( x in_meets_terms s,y,r,A iff x in_meets_terms s,y | B,r | B,A )