theorem tautsat: :: PL_AXIOM:27

for A being Element of PL-WFF holds
( A is tautology iff {} PL-WFF |= A )