theorem Th45: :: MODELC_3:45

for x being set
for v being LTL-formula holds
( x is Element of LTLStates v iff ex s being strict elementary LTLnode over v st s = x )