let A be QC-alphabet ; :: thesis: for P being QC-pred_symbol of A holds P is QC-pred_symbol of (the_arity_of P),A
let P be QC-pred_symbol of A; :: thesis: P is QC-pred_symbol of (the_arity_of P),A
set k = the_arity_of P;
set QCP = { Q where Q is QC-pred_symbol of A : the_arity_of Q = the_arity_of P } ;
P in { Q where Q is QC-pred_symbol of A : the_arity_of Q = the_arity_of P } ;
hence P is QC-pred_symbol of (the_arity_of P),A ; :: thesis: verum