theorem :: XBOOLEAN:25

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