let r be Real; :: thesis: for s, p being Surreal st r <> 0 holds
for x, y, z being Surreal st x is s,p,r _term & z is s,p,r _term & x <= y & y <= z holds
y is s,p,r _term
let s, p be Surreal; :: thesis: ( r <> 0 implies for x, y, z being Surreal st x is s,p,r _term & z is s,p,r _term & x <= y & y <= z holds
y is s,p,r _term )
assume A1: r <> 0 ; :: thesis: for x, y, z being Surreal st x is s,p,r _term & z is s,p,r _term & x <= y & y <= z holds
y is s,p,r _term
let x, y, z be Surreal; :: thesis: ( x is s,p,r _term & z is s,p,r _term & x <= y & y <= z implies y is s,p,r _term )
assume that
A2: ( x is s,p,r _term & z is s,p,r _term ) and
A3: ( x <= y & y <= z ) ; :: thesis: y is s,p,r _term
set N = No_omega^ p;
set R = uReal . r;
set sNR = s + ((uReal . r) * (No_omega^ p));
set X = x - (s + ((uReal . r) * (No_omega^ p)));
set Y = y - (s + ((uReal . r) * (No_omega^ p)));
set Z = z - (s + ((uReal . r) * (No_omega^ p)));
( |.(x - (s + ((uReal . r) * (No_omega^ p)))).| infinitely< No_omega^ p & |.(z - (s + ((uReal . r) * (No_omega^ p)))).| infinitely< No_omega^ p ) by A2, Th73;
then A4: |.(x - (s + ((uReal . r) * (No_omega^ p)))).| + |.(z - (s + ((uReal . r) * (No_omega^ p)))).| infinitely< No_omega^ p by Th18;
( x - (s + ((uReal . r) * (No_omega^ p))) <= y - (s + ((uReal . r) * (No_omega^ p))) & y - (s + ((uReal . r) * (No_omega^ p))) <= z - (s + ((uReal . r) * (No_omega^ p))) ) by A3, SURREALR:43;
then |.(y - (s + ((uReal . r) * (No_omega^ p)))).| infinitely< No_omega^ p by A4, Th11, Th51;
hence y is s,p,r _term by A1, Th73; :: thesis: verum