:: deftheorem defines ExistGlobal MODELC_1:def 18 :
for H being CTL-formula holds
( H is ExistGlobal iff ex H1 being CTL-formula st H = EG H1 );