:: deftheorem Def59 defines |= MODELC_1:def 59 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for s being Element of S
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f iff (Fid (f,S)) . s = TRUE );