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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:{(7 + k)},(QC-symbols A):] or y in QC-pred_symbols A )
assume A1: y in [:{(7 + k)},(QC-symbols A):] ; :: thesis: y in QC-pred_symbols A
reconsider y1 = y `1 as Nat by MCART_1:12, A1;
reconsider y2 = y `2 as QC-symbol of A by A1, MCART_1:12;
y `1 = 7 + k by A1, MCART_1:12;
then 7 <= y1 by NAT_1:12;
then [y1,y2] in { [m,x] where m is Nat, x is QC-symbol of A : 7 <= m } ;
hence y in QC-pred_symbols A by A1, MCART_1:21; :: thesis: verum

end;

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

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { P where P is QC-pred_symbol of A : the_arity_of P = k } )
assume A2: x in X ; :: thesis: x in { P where P is QC-pred_symbol of A : the_arity_of P = k }
then reconsider Q = x as QC-pred_symbol of A ;
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 Def8;
hence x in { P where P is QC-pred_symbol of A : the_arity_of P = k } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { P where P is QC-pred_symbol of A : the_arity_of P = k } or x in X )
assume x in { P where P is QC-pred_symbol of A : the_arity_of P = k } ; :: thesis: x in X
then consider P being QC-pred_symbol of A such that
A3: x = P and
A4: the_arity_of P = k ;
P `1 = 7 + k by A4, Def8;
then A5: P `1 in {(7 + k)} by TARSKI:def 1;
A6: QC-pred_symbols A c= [:NAT,(QC-symbols A):] by Th6;
then P in [:NAT,(QC-symbols A):] ;
then P `2 in QC-symbols A 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 { P where P is QC-pred_symbol of A : the_arity_of P = k } is Subset of (QC-pred_symbols A) ; :: thesis: verum