theorem Th1: :: SURREALI:1

for o being object
for Inv being Function holds
( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} )