let x be Surreal; :: thesis: 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 )
let r be Sequence of REAL ; :: thesis: 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 )
let y, s be Sequence; :: thesis: 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 )
let alpha, B be Ordinal; :: thesis: ( alpha c= B implies ( x in_meets_terms s,y,r,alpha iff x in_meets_terms s,y | B,r | B,alpha ) )
assume A1: alpha c= B ; :: thesis: ( x in_meets_terms s,y,r,alpha iff x in_meets_terms s,y | B,r | B,alpha )
thus ( x in_meets_terms s,y,r,alpha implies x in_meets_terms s,y | B,r | B,alpha ) :: thesis: ( x in_meets_terms s,y | B,r | B,alpha implies x in_meets_terms s,y,r,alpha )

proof

assume A2: x in_meets_terms s,y,r,alpha ; :: thesis: x in_meets_terms s,y | B,r | B,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 | B) . beta holds
x is sb,yb,(r | B) . beta _term
let sb, yb be Surreal; :: thesis: ( beta in alpha & sb = s . beta & yb = (y | B) . beta implies x is sb,yb,(r | B) . beta _term )
assume A3: ( beta in alpha & sb = s . beta & yb = (y | B) . beta ) ; :: thesis: x is sb,yb,(r | B) . beta _term
( (r | B) . beta = r . beta & yb = y . beta ) by A1, A3, FUNCT_1:49;
hence x is sb,yb,(r | B) . beta _term by A2, A3; :: thesis: verum

end;

assume A4: x in_meets_terms s,y | B,r | B,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 A5: ( beta in alpha & sb = s . beta & yb = y . beta ) ; :: thesis: x is sb,yb,r . beta _term
( (r | B) . beta = r . beta & yb = (y | B) . beta ) by A5, A1, FUNCT_1:49;
hence x is sb,yb,r . beta _term by A4, A5; :: thesis: verum