theorem :: XBOOLEAN:18

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