let A be QC-alphabet ; :: thesis: QC-pred_symbols A c= [:NAT,(QC-symbols A):]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in QC-pred_symbols A or y in [:NAT,(QC-symbols A):] )
assume y in QC-pred_symbols A ; :: thesis: y in [:NAT,(QC-symbols A):]
then consider k being Nat, x being QC-symbol of A such that
A1: ( y = [k,x] & 7 <= k ) ;
k in NAT by ORDINAL1:def 12;
hence y in [:NAT,(QC-symbols A):] by ZFMISC_1:def 2, A1; :: thesis: verum