let F, H be LTL-formula; :: thesis: ( F is next implies ( H is_immediate_constituent_of F iff H = the_argument_of F ) )
assume F is next ; :: thesis: ( H is_immediate_constituent_of F iff H = the_argument_of F )
then F = 'X' (the_argument_of F) by Th5;
hence ( H is_immediate_constituent_of F iff H = the_argument_of F ) by Th14; :: thesis: verum