let Y be non empty set ; :: thesis: for b, a being Element of Funcs Y,BOOLEAN holds (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y
let b, a be Element of Funcs Y,BOOLEAN ; :: thesis: (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y
(('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = ('not' (('not' b) 'imp' ('not' a))) 'or' (a 'imp' b) by BVFUNC_4:8
.= ('not' (('not' ('not' b)) 'or' ('not' a))) 'or' (a 'imp' b) by BVFUNC_4:8
.= (('not' b) '&' ('not' ('not' a))) 'or' (a 'imp' b) by BVFUNC_1:16
.= (('not' b) '&' a) 'or' (('not' a) 'or' b) by BVFUNC_4:8
.= ((('not' b) '&' a) 'or' ('not' a)) 'or' b by BVFUNC_1:11
.= ((('not' b) 'or' ('not' a)) '&' (a 'or' ('not' a))) 'or' b by BVFUNC_1:14
.= ((('not' b) 'or' ('not' a)) '&' (I_el Y)) 'or' b by BVFUNC_4:6
.= (('not' b) 'or' ('not' a)) 'or' b by BVFUNC_1:9
.= ('not' a) 'or' (('not' b) 'or' b) by BVFUNC_1:11
.= ('not' a) 'or' (I_el Y) by BVFUNC_4:6 ;
hence (('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y by BVFUNC_1:13; :: thesis: verum