theorem :: PL_AXIOM:37

for p, q being Element of PL-WFF holds (p 'or' q) <=> (q 'or' p) is tautology