:: deftheorem defines 'X' MODELC_2:def 36 :
for V being LTLModel
for f being Assign of V holds 'X' f = the NEXT of V . f;