theorem Th20: :: SURREALI:20

for x being Surreal st x is positive holds
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x)