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) => ((SAT M) . (q => p)) by Def11
.= ((SAT M) . p) => (((SAT M) . q) => ((SAT M) . p)) by Def11
.= 1 by XBOOLEAN:104 ; :: thesis: verum