theorem Th4: :: SURREALS:4

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