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