consider B being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ being second_Q_comp of B such that
A2: ( S = Sub_All B,SQ & B `1 = Sub_the_scope_of S & B is quantifiable ) by A1, SUBSTUT1:def 34;
S `1 = All (B `2 ),((B `1 ) `1 ) by A2, Th27;
then (B `1 ) `1 is Element of CQC-WFF by CQC_LANG:23;
then consider S1 being Element of QC-Sub-WFF such that
A3: ( S1 = B `1 & S1 `1 is Element of CQC-WFF ) ;
B `1 in CQC-Sub-WFF by A3, SUBSTUT1:def 39;
hence Sub_the_scope_of S is Element of CQC-Sub-WFF by A2; :: thesis: verum