let F, H be LTL-formula; :: thesis:
assume A1: H is_immediate_constituent_of F ; :: thesis:
thus H is_subformula_of F :: according to MODELC_2:def 23 :: thesis:

take n = 2; :: according to MODELC_2:def 22 :: thesis:
take L = <*H,F*>; :: thesis:
thus 1 <= n ; :: thesis:
thus len L = n by FINSEQ_1:44; :: thesis:
thus ( L . 1 = H & L . n = F ) ; :: thesis:
let k be Nat; :: thesis:
assume that
A2: 1 <= k and
A3: k < n ; :: thesis:
take H ; :: thesis:
take F ; :: thesis:
k < 1 + 1 by A3;
then k <= 1 by NAT_1:13;
then k = 1 by A2, XXREAL_0:1;
hence ( L . k = H & L . (k + 1) = F ) ; :: thesis:
thus H is_immediate_constituent_of F by A1; :: thesis:

end;

assume H = F ; :: thesis:
then len H = len F ;
hence contradiction by A1, Th28; :: thesis: