let F, H be ZF-formula; ( H is_proper_subformula_of F implies len H < len F )
assume
H is_subformula_of F
; ZF_LANG:def 41 ( not H <> F or len H < len F )
then consider n being Element of 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 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 )
;
defpred S1[ Nat] means ( 1 <= $1 & $1 < n implies for H1 being ZF-formula st L . ($1 + 1) = H1 holds
len H < len H1 );
A5:
for k being Nat st S1[k] holds
S1[k + 1]
assume
H <> F
; 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:
S1[ 0 ]
;
A16:
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A5);
reconsider k = k as Element of NAT by ORDINAL1:def 12;
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; verum