let v be LTL-formula; :: thesis: init v is Element of LTLStates v
init v is Element of LTLNodes v by Def30;
then init v in LTLStates v ;
hence init v is Element of LTLStates v ; :: thesis: verum