theorem Th15: :: PL_AXIOM:28

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