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

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

end;

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