theorem Th8: :: MODELC_1:8

for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai))