let x, y be Surreal; :: thesis: for r being Real st x is positive & |.(x - ((No_omega^ y) * (uReal . r))).| infinitely< x holds
r is positive
let r be Real; :: thesis: ( x is positive & |.(x - ((No_omega^ y) * (uReal . r))).| infinitely< x implies r is positive )
assume that
A1: ( x is positive & |.(x - ((No_omega^ y) * (uReal . r))).| infinitely< x ) and
A2: not r is positive ; :: thesis: contradiction
A3: 0_No <= x by A1;
A4: 0_No <= No_omega^ y by SURREALI:def 8;
uReal . r <= 0_No by A2, SURREALN:51, SURREALN:47;
then ( (No_omega^ y) * (uReal . r) <= (No_omega^ y) * 0_No & (No_omega^ y) * 0_No = 0_No ) by A4, SURREALR:75;
then - 0_No <= - ((No_omega^ y) * (uReal . r)) by SURREALR:10;
then A5: ( x + 0_No <= x + (- ((No_omega^ y) * (uReal . r))) & 0_No + 0_No <= x + (- ((No_omega^ y) * (uReal . r))) ) by A3, SURREALR:43;
|.(x + (- ((No_omega^ y) * (uReal . r)))).| < x by A1, Th9;
hence contradiction by A5, Def6; :: thesis: verum