let F, H be LTL-formula; :: thesis: ( F is Until implies ( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) ) )
assume F is Until ; :: 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) 'U' (the_right_argument_of F) by Th8;
hence ( H is_immediate_constituent_of F iff ( H = the_left_argument_of F or H = the_right_argument_of F ) ) by Th17; :: thesis: verum