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