theorem Th2: :: SURREALS:2

for o being object
for x being Surreal holds
( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) )