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