for A, B being Element of PL-WFF
for M being PLModel holds (SAT M) . (A <=> B) = ((SAT M) . A) <=> ((SAT M) . B)