let H, F be ZF-formula; :: thesis: ( H is_proper_subformula_of F implies len H < len F )
assume H is_subformula_of F ; :: according to ZF_LANG:def 41 :: thesis: ( not H <> F or len H < len F )
then consider n being Element of NAT , L being FinSequence such that
A1: ( 1 <= n & len L = n & L . 1 = H & L . n = F ) and
A2: 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;
assume H <> F ; :: thesis: len H < len F
then 1 < n by A1, XXREAL_0:1;
then A3: 1 + 1 <= n by NAT_1:13;
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 < n implies for H1 being ZF-formula st L . ($1 + 1) = H1 holds
len H < len H1 );
A4: S₁[ 0 ] ;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A6: ( 1 <= k & k < n implies for H1 being ZF-formula st L . (k + 1) = H1 holds
len H < len H1 ) and
A7: ( 1 <= k + 1 & k + 1 < n ) ; :: thesis: for H1 being ZF-formula st L . ((k + 1) + 1) = H1 holds
len H < len H1
let H1 be ZF-formula; :: thesis: ( L . ((k + 1) + 1) = H1 implies len H < len H1 )
assume A8: L . ((k + 1) + 1) = H1 ; :: thesis: len H < len H1
consider F1, G being ZF-formula such that
A9: ( L . (k + 1) = F1 & L . ((k + 1) + 1) = G & F1 is_immediate_constituent_of G ) by A2, A7;
A10: ( k = 0 implies len H < len H1 ) by A1, A8, A9, Th81;

now

given m being Nat such that A11: k = m + 1 ; :: thesis: len H < len H1
len H < len F1 by A6, A7, A9, A11, NAT_1:11, NAT_1:13;
hence len H < len H1 by A8, A9, Th81, XXREAL_0:2; :: thesis: verum

end;

hence len H < len H1 by A10, NAT_1:6; :: thesis: verum

end;

A12: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
consider k being Nat such that
A13: n = 2 + k by A3, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A14: (1 + 1) + k = (1 + k) + 1 ;
then ( 1 + k < n & 1 <= 1 + k ) by A13, NAT_1:11, NAT_1:13;
hence len H < len F by A1, A12, A13, A14; :: thesis: verum