let x be Surreal; :: thesis: ( x is positive implies ||.||.x.||.|| = ||.x.|| )
set Nx = ||.x.||;
set NNx = ||.||.x.||.||;
assume A1: x is positive ; :: thesis: ||.||.x.||.|| = ||.x.||
for o being object st o in L_ ||.||.x.||.|| holds
o in L_ ||.x.||

proof

let o be object ; :: thesis: ( o in L_ ||.||.x.||.|| implies o in L_ ||.x.|| )
assume A2: ( o in L_ ||.||.x.||.|| & not o in L_ ||.x.|| ) ; :: thesis: contradiction
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ ||.x.|| & o is positive ) ) by A2, Def9;
hence contradiction by A1, A2, Def9; :: thesis: verum

end;

then A3: L_ ||.||.x.||.|| c= L_ ||.x.|| by TARSKI:def 3;
for o being object st o in L_ ||.x.|| holds
o in L_ ||.||.x.||.||

proof

let o be object ; :: thesis: ( o in L_ ||.x.|| implies o in L_ ||.||.x.||.|| )
assume A4: ( o in L_ ||.x.|| & not o in L_ ||.||.x.||.|| ) ; :: thesis: contradiction
then reconsider o = o as Surreal by SURREAL0:def 16;
( o = 0_No or ( o in L_ x & o is positive ) ) by A1, A4, Def9;
hence contradiction by A4, Def9; :: thesis: verum

end;

then L_ ||.x.|| c= L_ ||.||.x.||.|| by TARSKI:def 3;
then A5: L_ ||.x.|| = L_ ||.||.x.||.|| by A3, XBOOLE_0:def 10;
for o being object st o in R_ ||.||.x.||.|| holds
o in R_ ||.x.||

proof

let o be object ; :: thesis: ( o in R_ ||.||.x.||.|| implies o in R_ ||.x.|| )
assume A6: ( o in R_ ||.||.x.||.|| & not o in R_ ||.x.|| ) ; :: thesis: contradiction
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ ||.x.|| & o is positive ) by A6, Def9;
hence contradiction by A6; :: thesis: verum

end;

then A7: R_ ||.||.x.||.|| c= R_ ||.x.|| by TARSKI:def 3;
for o being object st o in R_ ||.x.|| holds
o in R_ ||.||.x.||.||

proof

let o be object ; :: thesis: ( o in R_ ||.x.|| implies o in R_ ||.||.x.||.|| )
assume A8: ( o in R_ ||.x.|| & not o in R_ ||.||.x.||.|| ) ; :: thesis: contradiction
then reconsider o = o as Surreal by SURREAL0:def 16;
( o in R_ x & o is positive ) by A1, A8, Def9;
hence contradiction by A8, Def9; :: thesis: verum

end;

then R_ ||.x.|| c= R_ ||.||.x.||.|| by TARSKI:def 3;
then R_ ||.x.|| = R_ ||.||.x.||.|| by A7, XBOOLE_0:def 10;
hence ||.||.x.||.|| = ||.x.|| by A5, XTUPLE_0:2; :: thesis: verum