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

proof

let Q be object ; :: thesis: ( Q in QC-pred_symbols Al implies Q in QC-pred_symbols Al2 )
assume A1: Q in QC-pred_symbols Al ; :: thesis: Q in QC-pred_symbols Al2
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: verum

end;

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