let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in QC-pred_symbols or x in [:NAT ,NAT :] )
assume x in QC-pred_symbols ; :: thesis: x in [:NAT ,NAT :]
then ex k, l being Element of NAT st
( x = [k,l] & 7 <= k ) ;
hence x in [:NAT ,NAT :] by ZFMISC_1:def 2; :: thesis: verum