let x be Surreal; ( x is positive implies 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 ")))))] )
set Nx = ||.x.||;
set Inv = No_inverses_on ||.x.||;
assume A1:
x is positive
; 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 ")))))]
then
not x == 0_No
;
then A2:
x " = inv x
by A1, Def14;
set UL = Union (divL (||.x.||,(No_inverses_on ||.x.||)));
set UR = Union (divR (||.x.||,(No_inverses_on ||.x.||)));
A3:
inv x = [(Union (divL (||.x.||,(No_inverses_on ||.x.||)))),(Union (divR (||.x.||,(No_inverses_on ||.x.||))))]
by A1, Th26;
then
Union (divL (||.x.||,(No_inverses_on ||.x.||))) c= (L_ (x ")) \/ (R_ (x "))
by A2, XBOOLE_1:7;
then A4:
( divset ((Union (divL (||.x.||,(No_inverses_on ||.x.||)))),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) = divset ((R_ x),||.x.||,(Union (divL (||.x.||,(No_inverses_on ||.x.||))))) & divset ((Union (divL (||.x.||,(No_inverses_on ||.x.||)))),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) = divset ((L_ x),||.x.||,(Union (divL (||.x.||,(No_inverses_on ||.x.||))))) )
by A1, A2, A3, Th34;
Union (divR (||.x.||,(No_inverses_on ||.x.||))) c= (L_ (x ")) \/ (R_ (x "))
by A2, A3, XBOOLE_1:7;
then A5:
( divset ((Union (divR (||.x.||,(No_inverses_on ||.x.||)))),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)) = divset ((L_ x),||.x.||,(Union (divR (||.x.||,(No_inverses_on ||.x.||))))) & divset ((Union (divR (||.x.||,(No_inverses_on ||.x.||)))),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)) = divset ((R_ x),||.x.||,(Union (divR (||.x.||,(No_inverses_on ||.x.||))))) )
by A1, A2, A3, Th34;
Union (divL (||.x.||,(No_inverses_on ||.x.||))) = ({0_No} \/ (divset ((Union (divL (||.x.||,(No_inverses_on ||.x.||)))),||.x.||,(R_ ||.x.||),(No_inverses_on ||.x.||)))) \/ (divset ((Union (divR (||.x.||,(No_inverses_on ||.x.||)))),||.x.||,(L_ ||.x.||),(No_inverses_on ||.x.||)))
by Th12;
hence
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 A4, A5, A3, A2, Th13; verum