for G being LTL-formula st ( G is conjunctive or G is disjunctive or G is Until or G is Release ) holds
( the_left_argument_of G is_subformula_of G & the_right_argument_of G is_subformula_of G )