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