let p be Element of PL-WFF ; :: thesis: for M being PLModel holds (SAT M) . ('not' p) = 'not' ((SAT M) . p)
let M be PLModel; :: thesis: (SAT M) . ('not' p) = 'not' ((SAT M) . p)
thus (SAT M) . ('not' p) = ((SAT M) . p) => ((SAT M) . FaLSUM) by Def11
.= ((SAT M) . p) => FALSE by Def11
.= 'not' ((SAT M) . p) ; :: thesis: verum