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