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