for x, y being Element of BOOLEAN holds
( nand2 . <*x,y*> = 'not' (x '&' y) & nand2a . <*x,y*> = 'not' (('not' x) '&' y) & or2 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) by Def2, Def3, Lm1;