:: deftheorem defines SIGMA MODELC_1:def 63 :
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 being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : s |= f } ;