theorem :: PL_AXIOM:24

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