theorem semnot2: :: PL_AXIOM:19

for p being Element of PL-WFF
for M being PLModel holds (SAT M) . ('not' p) = 'not' ((SAT M) . p)