:: deftheorem defines EvalSet MODELC_1:def 31 :
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for n being Element of NAT holds EvalSet (V,Kai,n) = { h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;