theorem :: XBOOLEAN:12
for p, q being boolean object holds p 'or' (('not' p) '&' q) = p 'or' q