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:13;
hence CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF by A2, Th14, Th32; :: thesis: verum