let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' ('not' b)) = (('not' a) '&' b) 'or' (a '&' ('not' b))
let a, b be Element of Funcs 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_8:13; :: thesis: verum