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 is s, No_omega^ p,r _Term & z is s, No_omega^ p,r _Term ) by A2, Th73;
then y is s, No_omega^ p,r _Term by A3, Th74;
hence y is s,p,r _term by A1, Th73; :: thesis: verum