let F, H be LTL-formula; :: thesis: ( F is atomic implies not H is_immediate_constituent_of F )
assume F is atomic ; :: thesis: not H is_immediate_constituent_of F
then ( F . 1 <> 2 & F . 1 <> 3 & F . 1 <> 4 & F . 1 <> 5 & F . 1 <> 0 & F . 1 <> 1 ) by Lm9;
hence not H is_immediate_constituent_of F by Th12; :: thesis: verum