let F, G, H be ZF-formula; :: thesis: ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )
assume A1: ( F is_subformula_of G '&' H & F <> G '&' H ) ; :: according to ZF_LANG:def 41 :: thesis: ( F is_subformula_of G or F is_subformula_of H )
then consider n being Element of NAT , L being FinSequence such that
A2: ( 1 <= n & len L = n & L . 1 = F & L . n = G '&' H ) and
A3: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def40;
1 < n by A1, A2, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A4: n = 2 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:19;
(1 + 1) + k = (1 + k) + 1 ;
then ( 1 <= 1 + k & 1 + k < n ) by A4, NAT_1:11, NAT_1:13;
then consider H1, G1 being ZF-formula such that
A5: ( L . (1 + k) = H1 & L . ((1 + k) + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A3;
F is_subformula_of H1

proof

take m = 1 + k; :: according to ZF_LANG:def 40 :: thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-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 = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus A6: 1 <= m by NAT_1:11; :: thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-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 A2, A4, FINSEQ_1:21; :: thesis: ( L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )

A7: now

let j be Element of 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 Element of 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:72; :: thesis: verum

end;

hence L1 . 1 = F by A2, A6; :: thesis: ( L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus L1 . m = H1 by A5, A6, A7; :: thesis: for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being ZF-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be Element of NAT ; :: thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume A8: ( 1 <= j & j < m ) ; :: thesis: ex H1, F1 being ZF-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
then A9: ( 1 <= 1 + j & 1 + j = j + 1 & j <= m & j + 1 <= m ) by NAT_1:13;
m <= m + 1 by NAT_1:11;
then j < n by A4, A8, XXREAL_0:2;
then consider F1, G1 being ZF-formula such that
A10: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A3, A8;
take F1 ; :: thesis: ex F1 being ZF-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 )
thus ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A8, A9, A10; :: thesis: verum

end;

hence ( F is_subformula_of G or F is_subformula_of H ) by A2, A4, A5, Th72; :: thesis: verum