for A being Element of PL-WFF holds
( A is tautology iff {} PL-WFF |- A ) by tautsat, sth, ct;