let v be LTL-formula; :: thesis: for s being strict elementary LTLnode of v holds s is Element of LTLStates v
let s be strict elementary LTLnode of v; :: thesis: s is Element of LTLStates v
s is Element of LTLNodes v by defLTLNodes;
then s in LTLStates v ;
hence s is Element of LTLStates v ; :: thesis: verum