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;
A2: X <> {} by A1;
thus A3: NAT c= QC-symbols A by A1, A2, RELAT_1:160; :: thesis: 0 in QC-symbols A
0 in NAT ;
hence 0 in QC-symbols A by A3; :: thesis: verum