theorem th7a: :: PL_AXIOM:12

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