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

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

assume (SAT M) . (A 'or' B) = 1 ; :: thesis: ( (SAT M) . A = 1 or (SAT M) . B = 1 )
then ((SAT M) . A) 'or' ((SAT M) . B) = 1 by semdis2;
hence ( (SAT M) . A = 1 or (SAT M) . B = 1 ) by A2; :: thesis: verum

end;

assume A3: ( (SAT M) . A = 1 or (SAT M) . B = 1 ) ; :: thesis: (SAT M) . (A 'or' B) = 1
thus (SAT M) . (A 'or' B) = ((SAT M) . A) 'or' ((SAT M) . B) by semdis2
.= 1 by A3 ; :: thesis: verum