let F, H be LTL-formula; :: thesis: ( F is negative implies ( H is_immediate_constituent_of F iff H = the_argument_of F ) )
assume F is negative ; :: thesis: ( H is_immediate_constituent_of F iff H = the_argument_of F )
then F = 'not' (the_argument_of F) by Def18;
hence ( H is_immediate_constituent_of F iff H = the_argument_of F ) by Th13; :: thesis: verum