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