theorem :: SURREALS:5

for x being Surreal st 0_No <= x holds
NonNegativePart x == x