theorem :: SURREALI:38

for x being Surreal st x is positive holds
[(({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 ")))))] is Surreal