let F, H be LTL-formula; :: thesis: ( H is_proper_subformula_of F implies len H < len F )
assume H is_subformula_of F ; :: according to MODELC_2:def 23 :: thesis: ( not H <> F or len H < len F )
then consider n being Nat, L being FinSequence such that
A1: 1 <= n and
len L = n and
A2: L . 1 = H and
A3: L . n = F and
A4: 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 ) ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 < n implies for H1 being LTL-formula st L . ($1 + 1) = H1 holds
len H < len H1 );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A6: ( 1 <= k & k < n implies for H1 being LTL-formula st L . (k + 1) = H1 holds
len H < len H1 ) and
A7: 1 <= k + 1 and
A8: k + 1 < n ; :: thesis: for H1 being LTL-formula st L . ((k + 1) + 1) = H1 holds
len H < len H1
consider F1, G being LTL-formula such that
A9: L . (k + 1) = F1 and
A10: ( L . ((k + 1) + 1) = G & F1 is_immediate_constituent_of G ) by A4, A7, A8;
let H1 be LTL-formula; :: thesis: ( L . ((k + 1) + 1) = H1 implies len H < len H1 )
assume A11: L . ((k + 1) + 1) = H1 ; :: thesis: len H < len H1

A12: now :: thesis: ( ex m being Nat st k = m + 1 implies len H < len H1 )

given m being Nat such that A13: k = m + 1 ; :: thesis: len H < len H1
len H < len F1 by A6, A8, A9, A13, NAT_1:11, NAT_1:13;
hence len H < len H1 by A11, A10, Th28, XXREAL_0:2; :: thesis: verum

end;

( k = 0 implies len H < len H1 ) by A2, A11, A9, A10, Th28;
hence len H < len H1 by A12, NAT_1:6; :: thesis: verum

end;

assume H <> F ; :: thesis: len H < len F
then 1 < n by A1, A2, A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A14: n = 2 + k by NAT_1:10;
A15: S₁[ 0 ] ;
A16: for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A5);
A17: (1 + 1) + k = (1 + k) + 1 ;
then 1 + k < n by A14, NAT_1:13;
hence len H < len F by A3, A16, A14, A17, NAT_1:11; :: thesis: verum