theorem Th90: :: QC_LANG2:90

for A being QC-alphabet
for H being Element of QC-WFF A
for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}