let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y
let a be Function of Y,BOOLEAN; :: thesis: (('not' a) 'imp' a) 'eqv' a = I_el Y
(('not' a) 'imp' a) 'eqv' a = ((('not' a) 'imp' a) 'imp' a) '&' (a 'imp' (('not' a) 'imp' a)) by BVFUNC_4:7
.= (I_el Y) '&' (a 'imp' (('not' a) 'imp' a)) by BVFUNC_5:11
.= a 'imp' (('not' a) 'imp' a) by BVFUNC_1:6 ;
hence (('not' a) 'imp' a) 'eqv' a = I_el Y by Th21; :: thesis: verum