let Y be non empty set ; :: thesis: for a being Element of Funcs Y,BOOLEAN holds (('not' a) 'imp' a) 'eqv' a = I_el Y
let a be Element of Funcs 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:12
.= a 'imp' (('not' a) 'imp' a) by BVFUNC_1:9 ;
hence (('not' a) 'imp' a) 'eqv' a = I_el Y by Th22; :: thesis: verum