theorem Th33: :: PARTIT1:33

for Y being non empty set holds ERl (%O Y) = nabla Y