let A, B be Element of PL-WFF ; :: thesis: for M being PLModel holds
( (SAT M) . (A '&' B) = 1 iff ( (SAT M) . A = 1 & (SAT M) . B = 1 ) )
let M be PLModel; :: thesis: ( (SAT M) . (A '&' B) = 1 iff ( (SAT M) . A = 1 & (SAT M) . B = 1 ) )
hereby :: thesis: ( (SAT M) . A = 1 & (SAT M) . B = 1 implies (SAT M) . (A '&' B) = 1 )
assume (SAT M) . (A '&' B) = 1 ; :: thesis: ( (SAT M) . A = 1 & (SAT M) . B = 1 )
then ((SAT M) . A) '&' ((SAT M) . B) = 1 by semcon2;
hence ( (SAT M) . A = 1 & (SAT M) . B = 1 ) by XBOOLEAN:101; :: thesis: verum
end;
assume A3: ( (SAT M) . A = 1 & (SAT M) . B = 1 ) ; :: thesis: (SAT M) . (A '&' B) = 1
thus (SAT M) . (A '&' B) = ((SAT M) . A) '&' ((SAT M) . B) by semcon2
.= 1 by A3 ; :: thesis: verum