theorem :: BINARITH:6

for x, y being boolean object holds x '&' y = 'not' (('not' x) 'or' ('not' y)) ;