let H, F be Element of QC-WFF ; :: 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 21 :: thesis: ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF 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 Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF 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 Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus len L = n by FINSEQ_1:61; :: thesis: ( L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus ( L . 1 = H & L . n = F ) by FINSEQ_1:61; :: thesis: for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let k be Element of NAT ; :: thesis: ( 1 <= k & k < n implies ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume A2: ( 1 <= k & k < n ) ; :: thesis: ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
then k < 1 + 1 ;
then k <= 1 by NAT_1:13;
then A3: k = 1 by A2, XXREAL_0:1;
take H ; :: thesis: ex H1 being Element of QC-WFF 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 )
thus ( L . k = H & L . (k + 1) = F ) by A3, FINSEQ_1:61; :: thesis: H is_immediate_constituent_of F
thus H is_immediate_constituent_of F by A1; :: thesis: verum