for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for T being Subset of S holds SIGMA (Tau (T,R,BASSIGN)) = T