let o be object ; :: thesis: for x being Surreal holds
( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) )
let x be Surreal; :: thesis: ( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) )
A1: ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) )

proof

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

end;

( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) )

proof

assume x in R_ (NonNegativePart o) ; :: thesis: ( x in R_ o & 0_No <= x )
then ex l being Surreal st
( x = l & l in R_ o & 0_No <= l ) by Def1;
hence ( x in R_ o & 0_No <= x ) ; :: thesis: verum

end;

hence ( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) ) by A1, Def1; :: thesis: verum