theorem :: BVFUNC25:92

for Y being non empty set holds (O_el Y) 'eqv' (I_el Y) = O_el Y