let y be Surreal; :: thesis: for xL, x being Surreal st xL <= x & xL, No_omega^ y are_commensurate & not x, No_omega^ y are_commensurate holds
No_omega^ y infinitely< x
set O = No_omega^ y;
let xL, x be Surreal; :: thesis: ( xL <= x & xL, No_omega^ y are_commensurate & not x, No_omega^ y are_commensurate implies No_omega^ y infinitely< x )
assume that
A1: ( xL <= x & xL, No_omega^ y are_commensurate ) and
A2: not x, No_omega^ y are_commensurate and
A3: not No_omega^ y infinitely< x ; :: thesis: contradiction
consider r being positive Real such that
A4: not (No_omega^ y) * (uReal . r) < x by A3;
consider n being Nat such that
A5: r < n by SEQ_4:3;
reconsider n = n as positive Nat by A5;
A6: No_omega^ y is positive ;
( uReal . r < uReal . n & uReal . n = uDyadic . n & uDyadic . n = uInt . n ) by A5, SURREALN:51, SURREALN:46, SURREALN:def 5;
then (No_omega^ y) * (uReal . r) < (No_omega^ y) * (uInt . n) by A6, SURREALR:70;
then A7: x < (No_omega^ y) * (uInt . n) by A4, SURREALO:4;
consider k being positive Nat such that
A8: No_omega^ y < (uInt . k) * xL by A1;
uInt . k is positive ;
then 0_No <= uInt . k ;
then (uInt . k) * xL <= (uInt . k) * x by A1, SURREALR:75;
then No_omega^ y < (uInt . k) * x by A8, SURREALO:4;
hence contradiction by A2, A7; :: thesis: verum