let x, y be Surreal; :: thesis: ( x is positive & y in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} implies y is positive )
assume A1: ( x is positive & y in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ) ; :: thesis: y is positive
then A2: ( y in (L_ ||.x.||) \/ (R_ ||.x.||) & y <> 0_No ) by ZFMISC_1:56;
( y in L_ ||.x.|| or y in R_ ||.x.|| ) by A1, XBOOLE_0:def 3;
hence y is positive by Def9, A1, A2; :: thesis: verum