set IT = { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;
init v is Element of LTLNodes v by Def30;
then init v in { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } ;
hence { x where x is Element of LTLNodes v : x is strict elementary LTLnode over v } is non empty set ; :: thesis: verum