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 and
A3: B `1 = Sub_the_scope_of S and
A4: B is quantifiable by A1, SUBSTUT1:def 34;
S `1 = All (B `2 ),((B `1 ) `1 ) by A2, A4, Th27;
then (B `1 ) `1 is Element of CQC-WFF by CQC_LANG:23;
then B `1 in CQC-Sub-WFF by SUBSTUT1:def 39;
hence Sub_the_scope_of S is Element of CQC-Sub-WFF by A3; :: thesis: verum