theorem Th7: :: SURREALI:7

for o being object
for x being Surreal
for X being set
for Inv being Function holds divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)