:: deftheorem Def11 defines elementary MODELC_3:def 11 :
for v being LTL-formula
for N being LTLnode over v holds
( N is elementary iff the LTLnew of N = {} );