theorem :: BVFUNC25:93

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