:: deftheorem defines EX MODELC_1:def 35 :
for V being CTLModel
for f being Assign of V holds EX f = the EneXt of V . f;