consider x being bound_QC-variable of Al, F1 being QC-formula of Al 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 Al by CQC_LANG:8;
then A3: 'not' F1 is Element of CQC-WFF Al by CQC_LANG:13;
take F1 ; :: thesis: ( F1 is Element of CQC-WFF Al & ex x being bound_QC-variable of Al st p = Ex (x,F1) )
thus ( F1 is Element of CQC-WFF Al & ex x being bound_QC-variable of Al st p = Ex (x,F1) ) by A2, A3, CQC_LANG:8; :: thesis: verum