for F, H being LTL-formula st F is disjunctive holds
( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )