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