theorem :: PL_AXIOM:33

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