let A be QC-alphabet ; :: thesis: QC-pred_symbols A c= [:NAT,(QC-symbols A):]
let y be set ; :: 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 ex k being Element of NAT ex x being QC-symbol of A st
( y = [k,x] & 7 <= k ) ;
hence y in [:NAT,(QC-symbols A):] by ZFMISC_1:def 2; :: thesis: verum