consider B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):], SQ being second_Q_comp of B such that
A2: S = Sub_All (B,SQ) and
A3: B `1 = Sub_the_scope_of S and
A4: B is quantifiable by A1, 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 A5: 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 A2, A4, 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 A5, A3; :: thesis: verum