:: deftheorem defines EU MODELC_1:def 37 :
for V being CTLModel
for f, g being Assign of V holds f EU g = the EUntill of V . (f,g);