:: deftheorem defines is_immediate_constituent_of QC_LANG2:def 19 :
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( G is_immediate_constituent_of H iff ( H = 'not' G or ex F being Element of QC-WFF A st
( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable of A st H = All (x,G) ) );