theorem Th36: :: SURREALI:36

for x being Surreal st x is positive holds
x " = [(({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x "))))),((divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))))]