theorem Th23: :: QC_LANG3:23

for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A holds
( All (x,p) is closed iff still_not-bound_in p c= {x} )