let x be Surreal; :: thesis: ( x is positive implies for y1, y2 being Surreal st x, No_omega^ y1 are_commensurate & x, No_omega^ y2 are_commensurate holds
y1 <= y2 )
assume x is positive ; :: thesis: for y1, y2 being Surreal st x, No_omega^ y1 are_commensurate & x, No_omega^ y2 are_commensurate holds
y1 <= y2
let y1, y2 be Surreal; :: thesis: ( x, No_omega^ y1 are_commensurate & x, No_omega^ y2 are_commensurate implies y1 <= y2 )
assume that
A1: ( x, No_omega^ y1 are_commensurate & x, No_omega^ y2 are_commensurate ) and
A2: y2 < y1 ; :: thesis: contradiction
No_omega^ y2 infinitely< No_omega^ y1 by Lm5, A2;
then x infinitely< No_omega^ y1 by Th15, A1;
then x < x by Th9, Th16, A1;
hence contradiction by SURREALO:3; :: thesis: verum