theorem :: BINARITH:4

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