theorem Th50: :: MODELC_3:50

for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary holds
for k being Nat st not CastNode (((f |** k) . x),v) is elementary & w |= * (CastNode (((f |** k) . x),v)) holds
w |= * (CastNode (((f |** (k + 1)) . x),v))