theorem :: TWOSCOMP:59

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