now :: thesis: for o being object st o in R_ (NonNegativePart x) holds
o is surreal

let o be object ; :: thesis: ( o in R_ (NonNegativePart x) implies o is surreal )
assume o in R_ (NonNegativePart x) ; :: thesis: o is surreal
then ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) by Def1;
hence o is surreal ; :: thesis: verum

end;

hence for b₁ being set st b₁ = R_ (NonNegativePart x) holds
b₁ is surreal-membered ; :: thesis: verum