let o be object ; :: thesis: 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) ) )
let x be Surreal; :: thesis: ( 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) ) )
thus ( o in R_ (No_omega^ x) implies ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) ) ) :: thesis: ( ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) ) implies o in R_ (No_omega^ x) )

proof

assume o in R_ (No_omega^ x) ; :: thesis: ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) )
then consider xR being Surreal, r being positive Real such that
A1: ( xR in R_ x & o = (No_omega^ xR) *' (uReal . r) ) by Lm4;
o = (No_omega^ xR) * (uReal . r) by A1;
hence ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) ) by A1; :: thesis: verum

end;

thus ( ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) ) implies o in R_ (No_omega^ x) ) by Lm4; :: thesis: verum