:: deftheorem Def70 defines TransEG MODELC_1:def 70 :
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))
for b₅ being V230() Function of (bool S),(bool S) holds
( b₅ = TransEG f iff for G being Subset of S holds b₅ . G = SigFaxTau (f,G,R,BASSIGN) );