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