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:13;
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