:: deftheorem defines |= PL_AXIOM:def 15 :
for M being PLModel
for p being Element of PL-WFF holds
( M |= p iff (SAT M) . p = 1 );