let x be Surreal; :: thesis: for X, nX being set
for Y being surreal-membered set st x is positive & ( ( X = L_ x & nX = L_ ||.x.|| ) or ( X = R_ x & nX = R_ ||.x.|| ) ) holds
divset (X,||.x.||,Y) = divset (Y,||.x.||,nX,(No_inverses_on ||.x.||))
set Nx = ||.x.||;
set Inv = No_inverses_on ||.x.||;
let X, X1 be set ; :: thesis: for Y being surreal-membered set st x is positive & ( ( X = L_ x & X1 = L_ ||.x.|| ) or ( X = R_ x & X1 = R_ ||.x.|| ) ) holds
divset (X,||.x.||,Y) = divset (Y,||.x.||,X1,(No_inverses_on ||.x.||))
let Y be surreal-membered set ; :: thesis: ( x is positive & ( ( X = L_ x & X1 = L_ ||.x.|| ) or ( X = R_ x & X1 = R_ ||.x.|| ) ) implies divset (X,||.x.||,Y) = divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) )
assume that
A1: x is positive and
A2: ( ( X = L_ x & X1 = L_ ||.x.|| ) or ( X = R_ x & X1 = R_ ||.x.|| ) ) ; :: thesis: divset (X,||.x.||,Y) = divset (Y,||.x.||,X1,(No_inverses_on ||.x.||))
thus divset (X,||.x.||,Y) c= divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) :: according to XBOOLE_0:def 10 :: thesis: divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) c= divset (X,||.x.||,Y)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset (X,||.x.||,Y) or o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) )
assume o in divset (X,||.x.||,Y) ; :: thesis: o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||))
then consider x1, y1 being Surreal such that
A3: ( 0_No < x1 & x1 in X & y1 in Y ) and
A4: o = (1_No + ((x1 - ||.x.||) * y1)) * (x1 ") by Def15;
A5: x1 is positive by A3;
not x1 == 0_No by A3;
then A6: x1 " = inv x1 by A5, Def14;
A7: x1 is positive by A3;
A8: 0_No <= 0_No ;
A9: x1 in X1 by A2, A3, A1, A7, Def9;
( x1 in L_ ||.x.|| or x1 in R_ ||.x.|| ) by A2, A3, A1, A7, Def9;
then x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by XBOOLE_0:def 3;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A8, A3, ZFMISC_1:56;
then o = (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' ((No_inverses_on ||.x.||) . x1) by A6, A4, Def13;
then o in divs (y1,||.x.||,X1,(No_inverses_on ||.x.||)) by A9, A8, A3, Def2;
hence o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) by A3, Def3; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) or o in divset (X,||.x.||,Y) )
assume o in divset (Y,||.x.||,X1,(No_inverses_on ||.x.||)) ; :: thesis: o in divset (X,||.x.||,Y)
then consider y1 being object such that
A10: ( y1 in Y & o in divs (y1,||.x.||,X1,(No_inverses_on ||.x.||)) ) by Def3;
reconsider y1 = y1 as Surreal by A10, SURREAL0:def 16;
consider x1 being object such that
A11: ( x1 in X1 & x1 <> 0_No & o = (1_No +' ((x1 +' (-' ||.x.||)) *' y1)) *' ((No_inverses_on ||.x.||) . x1) ) by A10, Def2;
reconsider x1 = x1 as Surreal by A2, A11, SURREAL0:def 16;
A12: ( x1 in X & x1 is positive ) by A2, A1, A11, Def9;
A13: not x1 == 0_No by A12;
A14: x1 " = inv x1 by A12, A13, Def14;
x1 in (L_ ||.x.||) \/ (R_ ||.x.||) by XBOOLE_0:def 3, A2, A11;
then x1 in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by A11, ZFMISC_1:56;
then o = (1_No + ((x1 - ||.x.||) * y1)) * (x1 ") by A11, A14, Def13;
hence o in divset (X,||.x.||,Y) by Def15, A12, A10; :: thesis: verum