for x, y being Element of BOOLEAN holds nor2 . <*x,y*> = ('not' x) '&' ('not' y) by Lm3;