theorem :: BVFUNC_6:63

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