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