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