theorem Th4: :: SURREALI:4

for x, y being Surreal
for X being set
for Inv being Function holds divs (y,x,X,Inv) is surreal-membered