let Al be QC-alphabet ; :: thesis:
let Al2 be Al -expanding QC-alphabet ; :: thesis:
for Q being object st Q in QC-pred_symbols Al holds
Q in QC-pred_symbols Al2

proof

let Q be object ; :: thesis:
assume A1: Q in QC-pred_symbols Al ; :: thesis:
set preds = { [k,b] where k is Nat, b is QC-symbol of Al : 7 <= k } ;
set preds2 = { [k,b2] where k is Nat, b2 is QC-symbol of Al2 : 7 <= k } ;
consider k being Nat, b being QC-symbol of Al such that
A2: ( Q = [k,b] & 7 <= k ) by A1;
b in QC-symbols Al2 by Th2, TARSKI:def 3;
hence Q in QC-pred_symbols Al2 by A2; :: thesis:

end;

hence QC-pred_symbols Al c= QC-pred_symbols Al2 ; :: thesis: