theorem Th24: :: SURREALI:24
for x being Surreal st x is positive holds
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x)