let r be Real; :: thesis: for s, p, 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: 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
A1: ( x is s,p,r _Term & z is s,p,r _Term ) and
A2: ( x <= y & y <= z ) ; :: thesis: y is s,p,r _Term
set N = p;
set R = uReal . r;
set sNR = s + ((uReal . r) * p);
set X = x - (s + ((uReal . r) * p));
set Y = y - (s + ((uReal . r) * p));
set Z = z - (s + ((uReal . r) * p));
A3: |.(x - (s + ((uReal . r) * p))).| + |.(z - (s + ((uReal . r) * p))).| infinitely< p by A1, Th18;
( x - (s + ((uReal . r) * p)) <= y - (s + ((uReal . r) * p)) & y - (s + ((uReal . r) * p)) <= z - (s + ((uReal . r) * p)) ) by A2, SURREALR:43;
hence y is s,p,r _Term by A3, Th11, Th51; :: thesis: verum