theorem :: XBOOLEAN:21

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