theorem :: XBOOLEAN:22

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