consider x being bound_QC-variable, F1 being QC-formula such that
A2: p = Ex x,F1 by A1, QC_LANG2:def 13;
p = 'not' (All x,('not' F1)) by A2, QC_LANG2:def 5;
then All x,('not' F1) is Element of CQC-WFF by CQC_LANG:18;
then A3: 'not' F1 is Element of CQC-WFF by CQC_LANG:23;
take F1 ; :: thesis: ( F1 is Element of CQC-WFF & ex x being bound_QC-variable st p = Ex x,F1 )
thus ( F1 is Element of CQC-WFF & ex x being bound_QC-variable st p = Ex x,F1 ) by A2, A3, CQC_LANG:18; :: thesis: verum