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

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

assume (SAT M) . (A => B) = 1 ; :: thesis: ( (SAT M) . A = 0 or (SAT M) . B = 1 )
then ((SAT M) . A) => ((SAT M) . B) = 1 by Def11;
hence ( (SAT M) . A = 0 or (SAT M) . B = 1 ) by A3; :: thesis: verum

end;

assume A4: ( (SAT M) . A = 0 or (SAT M) . B = 1 ) ; :: thesis: (SAT M) . (A => B) = 1
thus (SAT M) . (A => B) = ((SAT M) . A) => ((SAT M) . B) by Def11
.= 1 by A4 ; :: thesis: verum