theorem th6a: :: PL_AXIOM:10

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