:: deftheorem defines tautology PL_AXIOM:def 18 :
for A being Element of PL-WFF holds
( A is tautology iff for M being PLModel holds (SAT M) . A = 1 );