let F, H be LTL-formula; :: thesis: ( F is atomic implies not H is_immediate_constituent_of F )
assume A1: F is atomic ; :: thesis: not H is_immediate_constituent_of F
then A2: ( not F . 1 = 2 & not F . 1 = 3 ) by Lm9;
A3: ( not F . 1 = 4 & not F . 1 = 5 ) by A1, Lm9;
A4: ( not F . 1 = 0 & not F . 1 = 1 ) by A1, Lm9;

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 Def21;
hence contradiction by A4, A2, A3, Th12; :: thesis: verum

end;

hence not H is_immediate_constituent_of F ; :: thesis: verum