let A, B be Element of PL-WFF ; :: thesis: for M being PLModel holds (SAT M) . (A 'or' B) = ((SAT M) . A) 'or' ((SAT M) . B)
let M be PLModel; :: thesis: (SAT M) . (A 'or' B) = ((SAT M) . A) 'or' ((SAT M) . B)
thus (SAT M) . (A 'or' B) = ((SAT M) . ('not' A)) => ((SAT M) . B) by Def11
.= ((SAT M) . A) 'or' ((SAT M) . B) by semnot2 ; :: thesis: verum