theorem Th10: :: MODELC_1:10

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