let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_subformula_of F
let F, H be Element of QC-WFF A; :: thesis: ( H is_immediate_constituent_of F implies H is_subformula_of F )
assume A1: H is_immediate_constituent_of F ; :: thesis: H is_subformula_of F
take n = 2; :: according to QC_LANG2:def 20 :: thesis: ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L = <*H,F*>; :: thesis: ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus 1 <= n ; :: thesis: ( len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus len L = n by FINSEQ_1:44; :: thesis: ( L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus ( L . 1 = H & L . n = F ) ; :: thesis: for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let k be Nat; :: thesis: ( 1 <= k & k < n implies ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A2: 1 <= k and
A3: k < n ; :: thesis: ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
take H ; :: thesis: ex H1 being Element of QC-WFF A st
( L . k = H & L . (k + 1) = H1 & H is_immediate_constituent_of H1 )
take F ; :: thesis: ( L . k = H & L . (k + 1) = F & H is_immediate_constituent_of F )
k < 1 + 1 by A3;
then k <= 1 by NAT_1:13;
then k = 1 by A2, XXREAL_0:1;
hence ( L . k = H & L . (k + 1) = F ) ; :: thesis: H is_immediate_constituent_of F
thus H is_immediate_constituent_of F by A1; :: thesis: verum