theorem :: SURREALC:24

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