for v being LTL-formula
for s being strict elementary LTLnode over v holds s is Element of LTLStates v