theorem Th1: :: SURREALS:1

for o being object holds
( L_ (NonNegativePart o) c= L_ o & R_ (NonNegativePart o) c= R_ o )