let A, B be Element of PL-WFF ; :: thesis: for M being PLModel holds
( (SAT M) . (A <=> B) = 1 iff (SAT M) . A = (SAT M) . B )
let M be PLModel; :: thesis: ( (SAT M) . (A <=> B) = 1 iff (SAT M) . A = (SAT M) . B )
A2: ( (SAT M) . B = TRUE or (SAT M) . B = FALSE ) by XBOOLEAN:def 3;

hereby :: thesis: ( (SAT M) . A = (SAT M) . B implies (SAT M) . (A <=> B) = 1 )

assume (SAT M) . (A <=> B) = 1 ; :: thesis: (SAT M) . A = (SAT M) . B
then ((SAT M) . A) <=> ((SAT M) . B) = 1 by semequ2;
hence (SAT M) . A = (SAT M) . B by A2; :: thesis: verum

end;

assume A3: (SAT M) . A = (SAT M) . B ; :: thesis: (SAT M) . (A <=> B) = 1
thus (SAT M) . (A <=> B) = ((SAT M) . A) <=> ((SAT M) . B) by semequ2
.= 1 by A3, A2 ; :: thesis: verum