let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
let x be bound_QC-variable of A; :: thesis: for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
let S be Element of QC-Sub-WFF A; :: thesis: for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
let xSQ be second_Q_comp of [S,x]; :: thesis: ( CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable implies CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A )
set S9 = Sub_All ([S,x],xSQ);
assume that
A1: CQC_Sub S is Element of CQC-WFF A and
A2: [S,x] is quantifiable ; :: thesis: CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A
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)) ;
then Quant ((Sub_All ([S,x],xSQ)),(CQC_Sub (Sub_the_scope_of (Sub_All ([S,x],xSQ))))) is Element of CQC-WFF A by A1, CQC_LANG:13;
hence CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A by A2, Th14, Th32; :: thesis: verum