theorem Th25: :: SURREALC:25

for x, y being Surreal st x < y holds
No_omega^ x infinitely< No_omega^ y by Lm5;