theorem Th4: :: QC_LANG4:4
for A being QC-alphabet
for F being Element of QC-WFF A holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }