theorem th8a: :: PL_AXIOM:15

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