theorem Th52: :: MODELC_3:52

for n being Nat
for v being LTL-formula
for q being sequence of (LTLStates v) ex s being strict elementary LTLnode over v st s = CastNode ((q . n),v)