theorem Th33: :: MODELC_1:33

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )