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
( ( for s being Element of S holds
( s |= g iff s |= Fax (f,g) ) ) iff SIGMA g is_a_fixpoint_of TransEG f )