theorem th6: :: PL_AXIOM:9

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