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