let r be non-zero Sequence of REAL ; :: thesis: for p, s being Sequence
for alpha being Ordinal st alpha c= dom r holds
for x, y, z being Surreal st x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha holds
y in_meets_terms s,p,r,alpha
let p, s be Sequence; :: thesis: for alpha being Ordinal st alpha c= dom r holds
for x, y, z being Surreal st x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha holds
y in_meets_terms s,p,r,alpha
let alpha be Ordinal; :: thesis: ( alpha c= dom r implies for x, y, z being Surreal st x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha holds
y in_meets_terms s,p,r,alpha )
assume alpha c= dom r ; :: thesis: for x, y, z being Surreal st x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha holds
y in_meets_terms s,p,r,alpha
let x, y, z be Surreal; :: thesis: ( x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha implies y in_meets_terms s,p,r,alpha )
assume A1: ( x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha ) ; :: thesis: y in_meets_terms s,p,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 = p . beta holds
y is sb,yb,r . beta _term
let sb, yb be Surreal; :: thesis: ( beta in alpha & sb = s . beta & yb = p . beta implies y is sb,yb,r . beta _term )
assume A2: ( beta in alpha & sb = s . beta & yb = p . beta ) ; :: thesis: y is sb,yb,r . beta _term
( x is sb,yb,r . beta _term & z is sb,yb,r . beta _term ) by A1, A2;
hence y is sb,yb,r . beta _term by A1, Th74; :: thesis: verum