let x be bound_QC-variable; :: thesis: for S being Element of QC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF & [S,x] is quantifiable holds
CQC_Sub (Sub_All [S,x],xSQ) is Element of CQC-WFF
let S be Element of QC-Sub-WFF ; :: thesis: for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF & [S,x] is quantifiable holds
CQC_Sub (Sub_All [S,x],xSQ) is Element of CQC-WFF
let xSQ be second_Q_comp of [S,x]; :: thesis: ( CQC_Sub S is Element of CQC-WFF & [S,x] is quantifiable implies CQC_Sub (Sub_All [S,x],xSQ) is Element of CQC-WFF )
set S9 = Sub_All [S,x],xSQ;
assume that
A1: CQC_Sub S is Element of CQC-WFF and
A2: [S,x] is quantifiable ; :: thesis: CQC_Sub (Sub_All [S,x],xSQ) is Element of CQC-WFF
Sub_the_scope_of (Sub_All [S,x],xSQ) = [S,x] `1 by A2, Th21;
then Quant (Sub_All [S,x],xSQ),(CQC_Sub (Sub_the_scope_of (Sub_All [S,x],xSQ))) = All (S_Bound (@ (Sub_All [S,x],xSQ))),(CQC_Sub S) by MCART_1:7;
then Quant (Sub_All [S,x],xSQ),(CQC_Sub (Sub_the_scope_of (Sub_All [S,x],xSQ))) is Element of CQC-WFF by A1, CQC_LANG:23;
hence CQC_Sub (Sub_All [S,x],xSQ) is Element of CQC-WFF by A2, Th14, Th32; :: thesis: verum