let x be Surreal; ( x is positive implies [(({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 )
set Nx = ||.x.||;
assume A1:
x is positive
; [(({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
then
divset ((R_ x),x,(L_ (x "))) <=_ divset ((R_ x),||.x.||,(L_ (x ")))
by Th18, Th35;
then A2:
{0_No} \/ (divset ((R_ x),x,(L_ (x ")))) <=_ {0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))
by SURREALO:31;
divset ((L_ x),x,(R_ (x "))) <=_ divset ((L_ x),||.x.||,(R_ (x ")))
by A1, Th18, Th35;
then A3:
({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x ")))) <=_ ({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x "))))
by A2, SURREALO:31;
( divset ((L_ x),x,(L_ (x "))) <=_ divset ((L_ x),||.x.||,(L_ (x "))) & divset ((R_ x),x,(R_ (x "))) <=_ divset ((R_ x),||.x.||,(R_ (x "))) )
by A1, Th18, Th35;
then A4:
(divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))) <=_ (divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x "))))
by SURREALO:31;
[(({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
by A1, Th36;
hence
[(({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
by TARSKI:1, Th37, A3, A4; verum