:: deftheorem Def1 defines NonNegativePart SURREALS:def 1 :
for x being object
for b₂ being pair set holds
( b₂ = NonNegativePart x iff for o being object holds
( ( o in L_ b₂ implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ b₂ ) & ( o in R_ b₂ implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ b₂ ) ) );