for A, B being Element of PL-WFF
for M being PLModel holds
( (SAT M) . (A => B) = 1 iff ( (SAT M) . A = 0 or (SAT M) . B = 1 ) )