:: deftheorem Def11 defines SAT PL_AXIOM:def 14 :
for M being PLModel
for b₂ being Function of PL-WFF,BOOLEAN holds
( b₂ = SAT M iff ( b₂ . FaLSUM = 0 & ( for k being Element of NAT holds
( b₂ . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b₂ . (p => q) = (b₂ . p) => (b₂ . q) ) ) );