:: deftheorem defines is_subformula_of QC_LANG2:def 20 :
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( G is_subformula_of H iff ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( 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 ) ) ) );