set Y = {(7 + k)};
[:{(7 + k)},NAT:] c= QC-pred_symbols

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:{(7 + k)},NAT:] or x in QC-pred_symbols )
assume A1: x in [:{(7 + k)},NAT:] ; :: thesis: x in QC-pred_symbols
then reconsider x1 = x `1 , x2 = x `2 as Element of NAT by MCART_1:12;
x `1 = 7 + k by A1, MCART_1:12;
then 7 <= x1 by NAT_1:12;
then [x1,x2] in { [m,n] where m, n is Element of NAT : 7 <= m } ;
hence x in QC-pred_symbols by A1, MCART_1:21; :: thesis: verum

end;

then reconsider X = [:{(7 + k)},NAT:] as non empty Subset of QC-pred_symbols ;
X = { P where P is QC-pred_symbol : the_arity_of P = k }

proof

thus X c= { P where P is QC-pred_symbol : the_arity_of P = k } :: according to XBOOLE_0:def 10 :: thesis: { P where P is QC-pred_symbol : the_arity_of P = k } c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { P where P is QC-pred_symbol : the_arity_of P = k } )
assume A2: x in X ; :: thesis: x in { P where P is QC-pred_symbol : the_arity_of P = k }
then reconsider Q = x as QC-pred_symbol ;
x `1 in {(7 + k)} by A2, MCART_1:10;
then x `1 = 7 + k by TARSKI:def 1;
then the_arity_of Q = k by Def6;
hence x in { P where P is QC-pred_symbol : the_arity_of P = k } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { P where P is QC-pred_symbol : the_arity_of P = k } or x in X )
assume x in { P where P is QC-pred_symbol : the_arity_of P = k } ; :: thesis: x in X
then consider P being QC-pred_symbol such that
A3: x = P and
A4: the_arity_of P = k ;
P `1 = 7 + k by A4, Def6;
then A5: P `1 in {(7 + k)} by TARSKI:def 1;
A6: P in [:NAT,NAT:] by Th10, TARSKI:def 3;
then P `2 in NAT by MCART_1:10;
then [(P `1),(P `2)] in X by A5, ZFMISC_1:87;
hence x in X by A3, A6, MCART_1:21; :: thesis: verum

end;

hence not k -ary_QC-pred_symbols is empty ; :: thesis: verum