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