theorem :: XBOOLEAN:11

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