let F, H be ZF-formula; ( H is_proper_subformula_of F implies ex G being ZF-formula st G is_immediate_constituent_of F )
assume
H is_subformula_of F
; ZF_LANG:def 41 ( not H <> F or ex G being ZF-formula st G is_immediate_constituent_of 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 )
;
assume
H <> F
; ex G being ZF-formula st G is_immediate_constituent_of 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
A5:
n = 2 + k
by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(1 + 1) + k = (1 + k) + 1
;
then
1 + k < n
by A5, NAT_1:13;
then consider H1, F1 being ZF-formula such that
L . (1 + k) = H1
and
A6:
( L . ((1 + k) + 1) = F1 & H1 is_immediate_constituent_of F1 )
by A4, NAT_1:11;
take
H1
; H1 is_immediate_constituent_of F
thus
H1 is_immediate_constituent_of F
by A3, A5, A6; verum