theorem Th25: :: BVFUNC_5:25

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