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

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {0_No} or not r in R_ (NonNegativePart x) or not r <= l )
assume A3: ( l in {0_No} & r in R_ (NonNegativePart x) ) ; :: thesis: not r <= l
consider R being Surreal such that
A4: ( R = r & R in R_ x & 0_No <= R ) by A3, Def1;
( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then 0_No < R by A4, A1, SURREALO:4;
hence l < r by A3, A4, TARSKI:def 1; :: thesis: verum

end;

hence 0_No <= NonNegativePart x by A2, SURREAL0:43; :: thesis: verum