theorem Th2: :: BVFUNC_5:2

for Y being non empty set
for b being Function of Y,BOOLEAN st (I_el Y) 'imp' b = I_el Y holds
b = I_el Y