let p be Element of PL-WFF ; :: thesis: ('not' ('not' p)) <=> p is tautology
let M be PLModel; :: according to PL_AXIOM:def 18 :: thesis: (SAT M) . (('not' ('not' p)) <=> p) = 1
thus (SAT M) . (('not' ('not' p)) <=> p) = ((SAT M) . ('not' ('not' p))) <=> ((SAT M) . p) by semequ2
.= ('not' ((SAT M) . ('not' p))) <=> ((SAT M) . p) by semnot2
.= ('not' ('not' ((SAT M) . p))) <=> ((SAT M) . p) by semnot2
.= 1 by th2 ; :: thesis: verum