theorem Th1: :: CQC_LANG:1

for A being QC-alphabet
for x being set holds
( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) )