reconsider X = |.x.| as positive Surreal by A1, Th36;
set y = omega-y X;
A2: X = |.X.| by Th31, Def6;
not - x == 0_No by A1, SURREALR:24;
then not X == 0_No by A1, Def6;
then X, No_omega^ (omega-y X) are_commensurate by A2, Def7;
then consider s being positive Real such that
A3: |.(X - ((No_omega^ (omega-y X)) * (uReal . s))).| infinitely< X by Th54;

per cases ( X = x or X = - x ) by Def6;

suppose A4: X = x ; :: thesis: ex b₁ being non zero Real st |.(x - ((No_omega^ (omega-y x)) * (uReal . b₁))).| infinitely< |.x.|

take s ; :: thesis: |.(x - ((No_omega^ (omega-y x)) * (uReal . s))).| infinitely< |.x.|
thus |.(x - ((No_omega^ (omega-y x)) * (uReal . s))).| infinitely< |.x.| by A3, A4; :: thesis: verum

end;

suppose A5: X = - x ; :: thesis: ex b₁ being non zero Real st |.(x - ((No_omega^ (omega-y x)) * (uReal . b₁))).| infinitely< |.x.|

then A6: X + (- ((No_omega^ (omega-y X)) * (uReal . s))) = - (x + ((No_omega^ (omega-y X)) * (uReal . s))) by SURREALR:40;
take - s ; :: thesis: |.(x - ((No_omega^ (omega-y x)) * (uReal . (- s)))).| infinitely< |.x.|
- (uReal . (- s)) == uReal . (- (- s)) by SURREALN:56;
then ( - ((No_omega^ (omega-y X)) * (uReal . (- s))) = (No_omega^ (omega-y X)) * (- (uReal . (- s))) & (No_omega^ (omega-y X)) * (- (uReal . (- s))) == (No_omega^ (omega-y X)) * (uReal . s) ) by SURREALR:51, SURREALR:58;
then x + ((No_omega^ (omega-y X)) * (uReal . s)) == x + (- ((No_omega^ (omega-y X)) * (uReal . (- s)))) by SURREALR:43;
then X + (- ((No_omega^ (omega-y X)) * (uReal . s))) == - (x + (- ((No_omega^ (omega-y X)) * (uReal . (- s))))) by SURREALR:10, A6;
then ( |.(X + (- ((No_omega^ (omega-y X)) * (uReal . s)))).| == |.(- (x + (- ((No_omega^ (omega-y X)) * (uReal . (- s)))))).| & |.(- (x + (- ((No_omega^ (omega-y X)) * (uReal . (- s)))))).| == |.(x + (- ((No_omega^ (omega-y X)) * (uReal . (- s))))).| ) by Th48, Th39, Th38;
then |.(X + (- ((No_omega^ (omega-y X)) * (uReal . s)))).| == |.(x + (- ((No_omega^ (omega-y X)) * (uReal . (- s))))).| by SURREALO:4;
then |.(x + (- ((No_omega^ (omega-y X)) * (uReal . (- s))))).| infinitely< X by A3, Th17;
hence |.(x - ((No_omega^ (omega-y x)) * (uReal . (- s)))).| infinitely< |.x.| by A5, A1, Th56; :: thesis: verum

end;

end;