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) = ((SAT M) . (A => B)) '&' ((SAT M) . (B => A)) by semcon2
.= (((SAT M) . A) => ((SAT M) . B)) '&' ((SAT M) . (B => A)) by Def11
.= ((SAT M) . A) <=> ((SAT M) . B) by Def11 ; :: thesis: verum