let A be QC-alphabet ; :: thesis: ( NAT c= QC-symbols A & 0 in QC-symbols A )
consider X being set such that
A1: ( NAT c= X & A = [:NAT,X:] ) by Def1;
thus A2: NAT c= QC-symbols A by A1, RELAT_1:160; :: thesis: 0 in QC-symbols A
thus 0 in QC-symbols A by A2; :: thesis: verum