theorem Th8: :: SURREALI:8
for x being Surreal
for X, Y being set
for Inv being Function holds divset (Y,x,X,Inv) = divset (Y,x,(X \ {0_No}),Inv)