theorem Th4: :: QC_LANG1:4

for A being QC-alphabet holds QC-variables A c= [:NAT,(QC-symbols A):]