let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st H is_proper_subformula_of F holds
ex G being Element of QC-WFF A st G is_immediate_constituent_of F
let F, H be Element of QC-WFF A; :: thesis: ( H is_proper_subformula_of F implies ex G being Element of QC-WFF A st G is_immediate_constituent_of 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 ex G being Element of QC-WFF A st G is_immediate_constituent_of F )
assume H <> F ; :: thesis: ex G being Element of QC-WFF A 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 Nat ;
(1 + 1) + k = (1 + k) + 1 ;
then 1 + k < n by A5, NAT_1:13;
then consider H1, F1 being Element of QC-WFF A 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 ; :: thesis: H1 is_immediate_constituent_of F
thus H1 is_immediate_constituent_of F by A3, A5, A6; :: thesis: verum