:: deftheorem defines ExistNext MODELC_1:def 17 :
for H being CTL-formula holds
( H is ExistNext iff ex H1 being CTL-formula st H = EX H1 );