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

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

hence
QC-pred_symbols Al c= QC-pred_symbols Al2
; :: thesis: verum
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;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