theorem Th50: :: MODELC_2:50

for H being LTL-formula
for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))