let Y be non empty set ; :: thesis: for a, b being Element of Funcs (Y,BOOLEAN) holds a 'eqv' b = ('not' a) 'eqv' ('not' b)
let a, b be Element of Funcs (Y,BOOLEAN); :: thesis: a 'eqv' b = ('not' a) 'eqv' ('not' b)
thus ('not' a) 'eqv' ('not' b) = (('not' a) 'imp' ('not' b)) '&' (('not' b) 'imp' ('not' a)) by BVFUNC_4:7
.= (b 'imp' a) '&' (('not' b) 'imp' ('not' a)) by Th3
.= (b 'imp' a) '&' (a 'imp' b) by Th3
.= a 'eqv' b by BVFUNC_4:7 ; :: thesis: verum