:: deftheorem defines final MODELC_3:def 12 :
for v being LTL-formula
for N being LTLnode over v holds
( N is final iff ( N is elementary & the LTLnext of N = {} ) );