theorem Th51: :: MODELC_3:51

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_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode (((f |** i) . x),v) is elementary & CastNode (((f |** (i + 1)) . x),v) is_succ_of CastNode (((f |** i) . x),v) ) ) & CastNode (((f |** n) . x),v) is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode (((f |** i) . x),v)) ) )