let F, G be LTL-formula; :: thesis: ( ( G is negative or G is next ) & F is_proper_subformula_of G implies F is_subformula_of the_argument_of G )
assume that
A1: ( G is negative or G is next ) and
A2: F is_subformula_of G and
A3: F <> G ; :: according to MODELC_2:def 23 :: thesis: F is_subformula_of the_argument_of G
consider n being Nat, L being FinSequence such that
A4: 1 <= n and
A5: len L = n and
A6: L . 1 = F and
A7: L . n = G and
A8: 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 ) by A2;
1 < n by A3, A4, A6, A7, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A9: n = 2 + k by NAT_1:10;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k; :: according to MODELC_2:def 22 :: thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = the_argument_of G & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take L1 ; :: thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = the_argument_of G & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus A10: 1 <= m by NAT_1:11; :: thesis: ( len L1 = m & L1 . 1 = F & L1 . m = the_argument_of G & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A5, A9, FINSEQ_1:17; :: thesis: ( L1 . 1 = F & L1 . m = the_argument_of G & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )

A11: now :: thesis: for j being Nat st 1 <= j & j <= m holds
L1 . j = L . j

let j be Nat; :: thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; :: thesis: L1 . j = L . j
then j in { j1 where j1 is Nat : ( 1 <= j1 & j1 <= 1 + k ) } ;
then j in Seg (1 + k) by FINSEQ_1:def 1;
hence L1 . j = L . j by FUNCT_1:49; :: thesis: verum

end;

hence L1 . 1 = F by A6, A10; :: thesis: ( L1 . m = the_argument_of G & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
m < m + 1 by NAT_1:13;
then consider F1, G1 being LTL-formula such that
A12: L . m = F1 and
A13: ( L . (m + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A8, A9, NAT_1:11;
F1 = the_argument_of G by A1, A7, A9, A13, Th20, Th21;
hence L1 . m = the_argument_of G by A10, A11, A12; :: thesis: for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be Nat; :: thesis: ( 1 <= j & j < m implies ex H1, F1 being LTL-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that
A14: 1 <= j and
A15: j < m ; :: thesis: ex H1, F1 being LTL-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
m <= m + 1 by NAT_1:11;
then j < n by A9, A15, XXREAL_0:2;
then consider F1, G1 being LTL-formula such that
A16: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A8, A14;
take F1 ; :: thesis: ex F1 being LTL-formula st
( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 )
take G1 ; :: thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A14, A15, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A11, A14, A15, A16; :: thesis: verum