:: deftheorem Def33 defines EvalFamily MODELC_1:def 33 :
for V being CTLModel
for Kai being Function of atomic_WFF, 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 (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) ) );