theorem :: TWOSCOMP:56

for x, y being Element of BOOLEAN holds and2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) by Lm4;