theorem th8: :: PL_AXIOM:14

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