theorem Th13: :: SURREALI:13

for x being Surreal
for Inv being Function holds Union (divR (x,Inv)) = (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))