:: deftheorem defines 'U' MODELC_2:def 37 :
for V being LTLModel
for f, g being Assign of V holds f 'U' g = the UNTIL of V . (f,g);