:: deftheorem Def9 defines ||. SURREALI:def 9 :
for x being object st x is positive Surreal holds
for b₂ being positive Surreal holds
( b₂ = ||.x.|| iff for y being Surreal holds
( ( not y in L_ b₂ 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_ b₂ ) & ( y in R_ b₂ implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ b₂ ) ) );