theorem :: TWOSCOMP:58
for x, y, z being Element of BOOLEAN holds nor3 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) by Lm7;