theorem :: XBOOLEAN:24

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