let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x
let x be bound_QC-variable of Al; :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x )
set S1 = CQCSub_All ([S,x],xSQ);
assume A1: [S,x] is quantifiable ; :: thesis: Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x
then CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by Def5;
then CQCSub_All ([S,x],xSQ) is Sub_universal by A1, SUBSTUT1:14;
then consider B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):], SQ being second_Q_comp of B such that
A2: CQCSub_All ([S,x],xSQ) = Sub_All (B,SQ) and
A3: B `2 = Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) and
A4: B is quantifiable by SUBSTUT1:def 33;
[S,x] `2 = B `2 by A1, A2, A4, Th36;
hence Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x by A3; :: thesis: verum