let A be QC-alphabet ; 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; ( 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
; 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 S1[ 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 & S1[k] holds
ex m being Nat st
( m < k & S1[m] )
proof
A9:
Seg n = dom L
by A4, FINSEQ_1:def 3;
let k be
Nat;
( k <> 0 & S1[k] implies ex m being Nat st
( m < k & S1[m] ) )
assume that A10:
k <> 0
and A11:
S1[
k]
;
ex m being Nat st
( m < k & S1[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 &
S1[
m] )
by A11, A12, A15, A16, Th8;
verum
end;
A17:
ex k being Nat st S1[k]
S1[ 0 ]
from NAT_1:sch 7(A17, A8);
hence
H in rng (tree_of_subformulae F)
by A5; verum