:: deftheorem defines 'X' MODELC_3:def 18 :
for v being LTL-formula
for N being LTLnode over v holds 'X' N = LTLnode(# ({} v), the LTLnext of N,({} v) #);