:: deftheorem defines * MODELC_3:def 22 :
for v being LTL-formula
for N being strict LTLnode over v holds * N = ( the LTLold of N \/ the LTLnew of N) \/ ('X' (CastLTL the LTLnext of N));