:: deftheorem defines conjunctive MODELC_1:def 16 :
for H being CTL-formula holds
( H is conjunctive iff ex F, G being CTL-formula st H = F '&' G );