theorem Th7: :: MODELC_2:7

for H being LTL-formula st H is disjunctive holds
H = (the_left_argument_of H) 'or' (the_right_argument_of H)