let Al be QC-alphabet ; 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; 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; 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]; ( [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
; 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; verum