theorem :: PL_AXIOM:34

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