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