for x, y being Element of BOOLEAN holds
( nor2 . <*x,y*> = 'not' (x 'or' y) & nor2a . <*x,y*> = 'not' (('not' x) 'or' y) & and2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) by Def5, Def6, Lm4;