:: deftheorem defines Until MODELC_2:def 16 :
for H being LTL-formula holds
( H is Until iff ex F, G being LTL-formula st H = F 'U' G );