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
; ( 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; verum