reconsider X = x as Surreal by A1;
consider s being Surreal such that
A2: s == X and
A3: for z being Surreal holds
( z in L_ s iff ( z = 0_No or ( z in L_ x & 0_No < z ) ) ) and
A4: for z being Surreal holds
( z in R_ s iff ( z in R_ x & 0_No < z ) ) by Lm1, A1, Def8;
0_No < s by A2, A1, Def8, SURREALO:4;
then reconsider s = s as positive Surreal by Def8;
take s ; :: thesis: for y being Surreal holds
( ( not y in L_ s or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s ) & ( y in R_ s implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s ) )
thus for y being Surreal holds
( ( not y in L_ s or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ s ) & ( y in R_ s implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ s ) ) by A3, A4; :: thesis: verum