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