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