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