theorem semcon2: :: PL_AXIOM:21

for A, B being Element of PL-WFF
for M being PLModel holds (SAT M) . (A '&' B) = ((SAT M) . A) '&' ((SAT M) . B)