:: deftheorem Def60 defines |= MODELC_1:def 60 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN))
for s being Element of S
for H being CTL-formula holds
( s,kai |= H iff s |= Evaluate (H,kai) );