theorem Th5: :: MODELC_1:5

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