:: deftheorem defines ExistUntill MODELC_1:def 19 :
for H being CTL-formula holds
( H is ExistUntill iff ex F, G being CTL-formula st H = F EU G );