theorem :: QC_LANG1:5

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