CQCSub_the_scope_of S1 = Sub_the_scope_of S1 by A1, Def6;
then CQC_Sub S1 = Quant (S1,p) by A1, A2, SUBSTUT1:32;
hence Quant (S1,p) is Element of CQC-WFF Al ; :: thesis: verum