:: deftheorem defines LTLStates MODELC_3:def 31 :
for v being LTL-formula holds LTLStates v = { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;