let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
let a, b be Function of Y,BOOLEAN; :: thesis: (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
a 'xor' b = (('not' a) '&' b) 'or' (a '&' ('not' b)) by BVFUNC_4:9;
hence (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b)) by BVFUNC_6:86; :: thesis: verum