theorem Th67: :: SURREALC:67
for y being Surreal
for r being Real st r <> 0 holds
not (uReal . r) * (No_omega^ y) == 0_No