let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
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 ; :: 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 Def6;
then CQCSub_All ([S,x],xSQ) is Sub_universal by A1, SUBSTUT1:14;
then consider B being Element of [:QC-Sub-WFF,bound_QC-variables:], 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, Th37;
hence Sub_the_bound_of (CQCSub_All ([S,x],xSQ)) = x by A3, MCART_1:7; :: thesis: verum