let H, F be LTL-formula; :: thesis: ( H is_immediate_constituent_of F implies H is_proper_subformula_of F )
assume A1: H is_immediate_constituent_of F ; :: thesis: H is_proper_subformula_of F
thus H is_subformula_of F :: according to MODELC_2:def 23 :: thesis: H <> F

proof

take n = 2; :: according to MODELC_2:def 22 :: thesis: ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take L = <*H,F*>; :: thesis: ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus 1 <= n ; :: thesis: ( len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus len L = n by FINSEQ_1:61; :: thesis: ( L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus ( L . 1 = H & L . n = F ) by FINSEQ_1:61; :: thesis: for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let k be Nat; :: thesis: ( 1 <= k & k < n implies ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume A2: ( 1 <= k & k < n ) ; :: thesis: ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
then k < 1 + 1 ;
then k <= 1 by NAT_1:13;
then A3: k = 1 by A2, XXREAL_0:1;
take H ; :: thesis: ex F1 being LTL-formula st
( L . k = H & L . (k + 1) = F1 & H is_immediate_constituent_of F1 )
take F ; :: thesis: ( L . k = H & L . (k + 1) = F & H is_immediate_constituent_of F )
thus ( L . k = H & L . (k + 1) = F ) by A3, FINSEQ_1:61; :: thesis: H is_immediate_constituent_of F
thus H is_immediate_constituent_of F by A1; :: thesis: verum

end;

assume H = F ; :: thesis: contradiction
then ( len H = len F & len H < len F ) by A1, Th116;
hence contradiction ; :: thesis: verum