theorem Th1: :: GOEDCPUC:1

for Al being QC-alphabet ex s being set st
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [s,[x,p]] in QC-symbols Al