:: deftheorem Def34 defines EvalFamily MODELC_2:def 34 :
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for b₃ being non empty set holds
( b₃ = EvalFamily (V,Kai) iff for p being set holds
( p in b₃ iff ( p in bool (Funcs (LTL_WFF, the carrier of V)) & ex n being Nat st p = EvalSet (V,Kai,n) ) ) );