theorem Th20: :: QC_LANG4:20

for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )