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