theorem :: BINARITH:5

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