:: deftheorem Def35 defines Evaluate MODELC_2:def 35 :
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for H being LTL-formula
for b₄ being Assign of V holds
( b₄ = Evaluate (H,Kai) iff ex f being Function of LTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b₄ = f . H ) );