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