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