let x be Surreal; :: thesis: 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 )
let r be Sequence of REAL ; :: thesis: 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 )
let y, s be Sequence; :: thesis: for alpha being Ordinal holds
( x in_meets_terms s,y,r,alpha iff x in_meets_terms s | (succ alpha),y,r,alpha )
let alpha be Ordinal; :: thesis: ( x in_meets_terms s,y,r,alpha iff x in_meets_terms s | (succ alpha),y,r,alpha )
thus ( x in_meets_terms s,y,r,alpha implies x in_meets_terms s | (succ alpha),y,r,alpha ) :: thesis: ( x in_meets_terms s | (succ alpha),y,r,alpha implies x in_meets_terms s,y,r,alpha )

proof

assume A1: x in_meets_terms s,y,r,alpha ; :: thesis: x in_meets_terms s | (succ alpha),y,r,alpha
let beta be Ordinal; :: according to SURREALC:def 14 :: thesis: for sb, yb being Surreal st beta in alpha & sb = (s | (succ alpha)) . beta & yb = y . beta holds
x is sb,yb,r . beta _term
let sb, yb be Surreal; :: thesis: ( beta in alpha & sb = (s | (succ alpha)) . beta & yb = y . beta implies x is sb,yb,r . beta _term )
assume A2: ( beta in alpha & sb = (s | (succ alpha)) . beta & yb = y . beta ) ; :: thesis: x is sb,yb,r . beta _term
beta in succ alpha by A2, ORDINAL1:8;
then (s | (succ alpha)) . beta = s . beta by FUNCT_1:49;
hence x is sb,yb,r . beta _term by A1, A2; :: thesis: verum

end;

assume A3: x in_meets_terms s | (succ alpha),y,r,alpha ; :: thesis: x in_meets_terms s,y,r,alpha
let beta be Ordinal; :: according to SURREALC:def 14 :: thesis: for sb, yb being Surreal st beta in alpha & sb = s . beta & yb = y . beta holds
x is sb,yb,r . beta _term
let sb, yb be Surreal; :: thesis: ( beta in alpha & sb = s . beta & yb = y . beta implies x is sb,yb,r . beta _term )
assume A4: ( beta in alpha & sb = s . beta & yb = y . beta ) ; :: thesis: x is sb,yb,r . beta _term
beta in succ alpha by A4, ORDINAL1:8;
then (s | (succ alpha)) . beta = s . beta by FUNCT_1:49;
hence x is sb,yb,r . beta _term by A3, A4; :: thesis: verum