theorem :: PL_AXIOM:35

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