theorem Th23: :: SURREALC:23

for o being object
for x being Surreal holds
( o in R_ (No_omega^ x) iff ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) ) )