let A be QC-alphabet ; :: thesis: A = [:NAT,(QC-symbols A):]
consider X being set such that
A1: ( NAT c= X & A = [:NAT,X:] ) by Def1;
X <> {} by A1;
hence A = [:NAT,(QC-symbols A):] by A1, RELAT_1:160; :: thesis: verum