theorem :: BVFUNC25:19

for Y being non empty set
for a being Function of Y,BOOLEAN holds ('not' ('not' a)) 'imp' a = I_el Y by BVFUNC_5:7;