let A be Element of PL-WFF ; :: thesis: for M being PLModel holds
( (SAT M) . ('not' A) = 1 iff (SAT M) . A = 0 )
let M be PLModel; :: thesis: ( (SAT M) . ('not' A) = 1 iff (SAT M) . A = 0 )

hereby :: thesis: ( (SAT M) . A = 0 implies (SAT M) . ('not' A) = 1 )

assume (SAT M) . ('not' A) = 1 ; :: thesis: (SAT M) . A = 0
then 'not' ((SAT M) . A) = 1 by semnot2;
hence (SAT M) . A = 0 ; :: thesis: verum

end;

assume A2: (SAT M) . A = 0 ; :: thesis: (SAT M) . ('not' A) = 1
thus (SAT M) . ('not' A) = 'not' ((SAT M) . A) by semnot2
.= 1 by A2 ; :: thesis: verum