theorem th7: :: PL_AXIOM:11
for p, q, r being boolean object holds ((p '&' q) '&' r) <=> (p '&' (q '&' r)) = TRUE