theorem :: XBOOLEAN:8

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