for x, y, z being Element of BOOLEAN holds
( nand3 . <*x,y,z*> = 'not' ((x '&' y) '&' z) & nand3a . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) & nand3b . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) & or3 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) by Def12, Def13, Def14, Lm5;