let p, q, r be boolean object ; :: thesis: p '&' (q 'nor' r) = (p '&' ('not' q)) '&' ('not' r)
thus p '&' (q 'nor' r) = p '&' (('not' q) '&' ('not' r))
.= (p '&' ('not' q)) '&' ('not' r) ; :: thesis: verum