theorem :: TWOSCOMP:15

for x, y, z being Element of BOOLEAN holds
( nor3 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) & nor3a . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) & nor3b . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) & and3 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ) by Def17, Def18, Def19, Lm8;