let x, y be Surreal; ( x is positive & y = [(({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 ")))))] implies x " == y )
set Nx = ||.x.||;
assume A1:
x is positive
; ( not y = [(({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 ")))))] or x " == y )
then A2:
x == ||.x.||
by Th18;
then
divset ((R_ x),x,(L_ (x "))) <==> divset ((R_ x),||.x.||,(L_ (x ")))
by Th35;
then A3:
{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 A2, Th35;
then A4:
({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 A3, 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 A2, Th35;
then A5:
(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;
assume A6:
y = [(({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 ")))))]
; x " == y
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 ")))))]
by A1, Th36;
hence
x " == y
by SURREALO:29, A6, A4, A5; verum