theorem :: BVFUNC_6:31

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