theorem Th55: :: MODELC_2:55

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