theorem Th71: :: QC_LANG2:71

for A being QC-alphabet
for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_subformula_of H iff F is_proper_subformula_of All (x,H) )