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