let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_subformula_of G holds
H in rng (tree_of_subformulae F)
let F, G, H be Element of QC-WFF A; :: thesis: ( G in rng (tree_of_subformulae F) & H is_subformula_of G implies H in rng (tree_of_subformulae F) )
assume that
A1: G in rng (tree_of_subformulae F) and
A2: H is_subformula_of G ; :: thesis: H in rng (tree_of_subformulae F)
consider n being Nat, L being FinSequence such that
A3: 1 <= n and
A4: len L = n and
A5: L . 1 = H and
A6: L . n = G and
A7: for k being Nat st 1 <= k & k < n holds
ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A2, QC_LANG2:def 20;
defpred S₁[ Nat] means ex H9 being Element of QC-WFF A st
( H9 = L . ($1 + 1) & $1 + 1 in dom L & H9 in rng (tree_of_subformulae F) );
A8: for k being Nat st k <> 0 & S₁[k] holds
ex m being Nat st
( m < k & S₁[m] )

proof

A9: Seg n = dom L by A4, FINSEQ_1:def 3;
let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex m being Nat st
( m < k & S₁[m] ) )
assume that
A10: k <> 0 and
A11: S₁[k] ; :: thesis: ex m being Nat st
( m < k & S₁[m] )
consider m being Nat such that
A12: m + 1 = k by A10, NAT_1:6;
0 < k by A10;
then A13: 0 + 1 <= k by NAT_1:13;
Seg (len L) = dom L by FINSEQ_1:def 3;
then A14: k + 1 <= n by A4, A11, FINSEQ_1:1;
then ( k in NAT & k < n ) by NAT_1:13, ORDINAL1:def 12;
then A15: ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A7, A13;
k <= n by A14, NAT_1:13;
then A16: k in dom L by A13, A9, FINSEQ_1:1;
m < k by A12, NAT_1:13;
hence ex m being Nat st
( m < k & S₁[m] ) by A11, A12, A15, A16, Th8; :: thesis: verum

end;

A17: ex k being Nat st S₁[k]

proof

0 <> n by A3;
then A18: ex k being Nat st k + 1 = n by NAT_1:6;
Seg n = dom L by A4, FINSEQ_1:def 3;
hence ex k being Nat st S₁[k] by A1, A6, A18, FINSEQ_1:3; :: thesis: verum

end;

S₁[ 0 ] from NAT_1:sch 7(A17, A8);
hence H in rng (tree_of_subformulae F) by A5; :: thesis: verum