let x be Surreal; :: thesis: ( 0_No <= x implies NonNegativePart x == x )
set NN = NonNegativePart x;
assume A1: 0_No <= x ; :: thesis: NonNegativePart x == x
then A2: 0_No <= NonNegativePart x by Th4;
A3: L_ (NonNegativePart x) << {x}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ (NonNegativePart x) or not r in {x} or not r <= l )
assume A4: ( l in L_ (NonNegativePart x) & r in {x} ) ; :: thesis: not r <= l
( L_ (NonNegativePart x) c= L_ x & L_ x << {x} ) by Th1, SURREALO:11;
hence not r <= l by A4; :: thesis: verum

end;

A5: {(NonNegativePart x)} << R_ x

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {(NonNegativePart x)} or not r in R_ x or not r <= l )
assume A6: ( l in {(NonNegativePart x)} & r in R_ x ) ; :: thesis: not r <= l
( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then 0_No <= r by A6, A1, SURREALO:4;
then A7: r in R_ (NonNegativePart x) by A6, Def1;
assume r <= l ; :: thesis: contradiction
then r <= NonNegativePart x by A6, TARSKI:def 1;
then ( r in {r} & {r} << R_ (NonNegativePart x) ) by TARSKI:def 1, SURREAL0:43;
hence contradiction by A7, SURREALO:3; :: thesis: verum

end;

A8: L_ x << {(NonNegativePart x)}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ x or not r in {(NonNegativePart x)} or not r <= l )
assume A9: ( l in L_ x & r in {(NonNegativePart x)} ) ; :: thesis: not r <= l
assume A10: r <= l ; :: thesis: contradiction
then NonNegativePart x <= l by A9, TARSKI:def 1;
then 0_No <= l by A2, SURREALO:4;
then A11: l in L_ (NonNegativePart x) by A9, Def1;
L_ (NonNegativePart x) << {(NonNegativePart x)} by SURREALO:11;
hence contradiction by A10, A9, A11; :: thesis: verum

end;

{x} << R_ (NonNegativePart x)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {x} or not r in R_ (NonNegativePart x) or not r <= l )
assume A12: ( l in {x} & r in R_ (NonNegativePart x) ) ; :: thesis: not r <= l
( R_ (NonNegativePart x) c= R_ x & {x} << R_ x ) by Th1, SURREALO:11;
hence not r <= l by A12; :: thesis: verum

end;

hence NonNegativePart x == x by A5, A8, A3, SURREAL0:43; :: thesis: verum