:: deftheorem Def1 defines QC-alphabet QC_LANG1:def 1 :
for b₁ being set holds
( b₁ is QC-alphabet iff ( b₁ is non empty set & ex X being set st
( NAT c= X & b₁ = [:NAT,X:] ) ) );