theorem Th30: :: SURREALC:30

for y, 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