let x, y, z be Element of BOOLEAN ; :: thesis: nor3 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z)
thus nor3 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) by Def17
.= (('not' x) '&' ('not' y)) '&' ('not' z) ; :: thesis: verum