consider B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):], SQ being second_Q_comp of B such that
A1: S = Sub_All (B,SQ) and
A2: B `1 = Sub_the_scope_of S and
A3: B is quantifiable by X1, SUBSTUT1:def 34;
set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;
{ G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;
then A4: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds
G in CQC-Sub-WFF Al ;
S `1 = All ((B `2),((B `1) `1)) by A1, A3, Th26;
then (B `1) `1 is Element of CQC-WFF Al by CQC_LANG:13;
hence Sub_the_scope_of S is Element of CQC-Sub-WFF Al by A4, A2; :: thesis: verum