let o be object ; :: thesis: ( L_ (NonNegativePart o) c= L_ o & R_ (NonNegativePart o) c= R_ o )
thus L_ (NonNegativePart o) c= L_ o :: thesis: R_ (NonNegativePart o) c= R_ o

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in L_ (NonNegativePart o) or a in L_ o )
assume a in L_ (NonNegativePart o) ; :: thesis: a in L_ o
then ex l being Surreal st
( a = l & l in L_ o & 0_No <= l ) by Def1;
hence a in L_ o ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in R_ (NonNegativePart o) or a in R_ o )
assume a in R_ (NonNegativePart o) ; :: thesis: a in R_ o
then ex r being Surreal st
( a = r & r in R_ o & 0_No <= r ) by Def1;
hence a in R_ o ; :: thesis: verum