let x be Surreal; :: thesis: ( x is positive implies ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) )
assume A1: x is positive ; :: thesis: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} or a in (L_ x) \/ (R_ x) )
assume A2: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: a in (L_ x) \/ (R_ x)
then reconsider a = a as Surreal by SURREAL0:def 16;
A3: ( a in (L_ ||.x.||) \/ (R_ ||.x.||) & a <> 0_No ) by A2, ZFMISC_1:56;
( a in L_ ||.x.|| or a in R_ ||.x.|| ) by A2, XBOOLE_0:def 3;
then ( a in L_ x or a in R_ x ) by Def9, A1, A3;
hence a in (L_ x) \/ (R_ x) by XBOOLE_0:def 3; :: thesis: verum