theorem Th22: :: SURREALC:22

for o being object
for x being Surreal holds
( o in L_ (No_omega^ x) iff ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) )