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