let F, H be LTL-formula; :: thesis: ( F is conjunctive implies ( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) ) )
assume F is conjunctive ; :: thesis: ( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) )
then F = (the_left_argument_of F) '&' (the_right_argument_of F) by Th6;
hence ( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) ) by Th15; :: thesis: verum