:: deftheorem Def1 defines -expanding QC_TRANS:def 1 :
for Al, Al2 being QC-alphabet holds
( Al2 is Al -expanding iff Al c= Al2 );