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