theorem :: XBOOLEAN:16

for p, q being boolean object holds p '&' ('not' (p => q)) = p '&' ('not' q)