let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st H is_proper_subformula_of F holds
len (@ H) < len (@ F)
let F, H be Element of QC-WFF A; :: thesis: ( H is_proper_subformula_of F implies len (@ H) < len (@ F) )
given n being 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 Nat st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def 20,QC_LANG2:def 21 :: thesis: ( not H <> F or len (@ H) < len (@ F) )
defpred S₁[ Nat] means ( 1 <= $1 & $1 < n implies for H1 being Element of QC-WFF A st L . ($1 + 1) = H1 holds
len (@ H) < len (@ H1) );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A6: ( 1 <= k & k < n implies for H1 being Element of QC-WFF A st L . (k + 1) = H1 holds
len (@ H) < len (@ H1) ) and
A7: 1 <= k + 1 and
A8: k + 1 < n ; :: thesis: for H1 being Element of QC-WFF A st L . ((k + 1) + 1) = H1 holds
len (@ H) < len (@ H1)
consider F1, G being Element of QC-WFF A such that
A9: L . (k + 1) = F1 and
A10: ( L . ((k + 1) + 1) = G & F1 is_immediate_constituent_of G ) by A4, A7, A8;
let H1 be Element of QC-WFF A; :: thesis: ( L . ((k + 1) + 1) = H1 implies len (@ H) < len (@ H1) )
assume A11: L . ((k + 1) + 1) = H1 ; :: thesis: len (@ H) < len (@ H1)

A12: now :: thesis: ( ex m being Nat st k = m + 1 implies len (@ H) < len (@ H1) )

given m being Nat such that A13: k = m + 1 ; :: thesis: len (@ H) < len (@ H1)
len (@ H) < len (@ F1) by A6, A8, A9, A13, NAT_1:11, NAT_1:13;
hence len (@ H) < len (@ H1) by A11, A10, Th51, XXREAL_0:2; :: thesis: verum

end;

( k = 0 implies len (@ H) < len (@ H1) ) by A2, A11, A9, A10, Th51;
hence len (@ H) < len (@ H1) by A12, NAT_1:6; :: thesis: verum

end;

assume H <> F ; :: thesis: 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: S₁[ 0 ] ;
A16: for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A5);
reconsider k = k as Nat ;
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; :: thesis: verum