let x, y be Surreal; :: thesis: for r being Real
for s being Surreal st r <> 0 holds
( x is s,y,r _term iff |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y )
let r be Real; :: thesis: for s being Surreal st r <> 0 holds
( x is s,y,r _term iff |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y )
let s be Surreal; :: thesis: ( r <> 0 implies ( x is s,y,r _term iff |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y ) )
assume A1: r <> 0 ; :: thesis: ( x is s,y,r _term iff |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y )
set N = No_omega^ y;
set R = uReal . r;
set sNR = s + ((uReal . r) * (No_omega^ y));
set X = x - (s + ((uReal . r) * (No_omega^ y)));
(s + ((uReal . r) * (No_omega^ y))) - (s + ((uReal . r) * (No_omega^ y))) == 0_No by SURREALR:39;
then A2: ( (s + ((uReal . r) * (No_omega^ y))) + (x - (s + ((uReal . r) * (No_omega^ y)))) = x + ((s + ((uReal . r) * (No_omega^ y))) + (- (s + ((uReal . r) * (No_omega^ y))))) & x + ((s + ((uReal . r) * (No_omega^ y))) + (- (s + ((uReal . r) * (No_omega^ y))))) == x + 0_No & x + 0_No = x ) by SURREALR:37, SURREALR:43;
thus ( x is s,y,r _term implies |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y ) :: thesis: ( |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y implies x is s,y,r _term )

proof

assume x is s,y,r _term ; :: thesis: |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y
then (s + ((uReal . r) * (No_omega^ y))) + (x - (s + ((uReal . r) * (No_omega^ y)))) is s,y,r _term by A2, Th72;
hence |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y by Th71; :: thesis: verum

end;

assume |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y ; :: thesis: x is s,y,r _term
then (s + ((uReal . r) * (No_omega^ y))) + (x - (s + ((uReal . r) * (No_omega^ y)))) is s,y,r _term by A1, Th71;
hence x is s,y,r _term by A2, Th72; :: thesis: verum