theorem semdis2: :: PL_AXIOM:23

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