theorem Th12: :: SURREALI:12

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