theorem :: BVFUNC25:91

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