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 A1: ( not F . 1 = 0 & not F . 1 = 1 & not F . 1 = 2 & not F . 1 = 3 & not F . 1 = 4 & not F . 1 = 5 ) by Lm8;

now

assume H is_immediate_constituent_of F ; :: thesis: contradiction
then ( F = 'not' H or F = 'X' H or ex H1 being LTL-formula st
( F = H '&' H1 or F = H1 '&' H or F = H 'or' H1 or F = H1 'or' H or F = H 'U' H1 or F = H1 'U' H or F = H 'R' H1 or F = H1 'R' H ) ) by Def100;
hence contradiction by A1, Th100; :: thesis: verum

end;

hence not H is_immediate_constituent_of F ; :: thesis: verum