let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds a 'eqv' (a 'nor' b) = ('not' a) '&' b
let a, b be Function of Y,BOOLEAN; :: thesis: a 'eqv' (a 'nor' b) = ('not' a) '&' b
thus a 'eqv' (a 'nor' b) = ((a 'or' a) 'or' b) '&' (('not' a) 'or' ('not' (a 'or' b))) by Th64
.= ((a 'or' b) '&' ('not' a)) 'or' ((a 'or' b) '&' ('not' (a 'or' b))) by BVFUNC_1:12
.= ((a 'or' b) '&' ('not' a)) 'or' (O_el Y) by BVFUNC_4:5
.= (a 'or' b) '&' ('not' a) by BVFUNC_1:9
.= (a '&' ('not' a)) 'or' (b '&' ('not' a)) by BVFUNC_1:12
.= (O_el Y) 'or' (b '&' ('not' a)) by BVFUNC_4:5
.= ('not' a) '&' b by BVFUNC_1:9 ; :: thesis: verum