theorem Th3: :: PRE_CIRC:4

for I being set holds uncurry (I --> {}) = {}