:: deftheorem defines EvalSet MODELC_2:def 32 :
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for n being Nat holds EvalSet (V,Kai,n) = { h where h is Function of LTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;