let Al be QC-alphabet ; :: thesis:
let X be Subset of (CQC-WFF Al); :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
let x be bound_QC-variable of Al; :: thesis:
assume A1: X is with_examples ; :: thesis:
thus ( X |- Ex (x,p) implies ex y being bound_QC-variable of Al st X |- p . (x,y) ) :: thesis:

proof

assume X |- Ex (x,p) ; :: thesis:
then consider f1 being FinSequence of CQC-WFF Al such that
A2: rng f1 c= X and
A3: |- f1 ^ <*(Ex (x,p))*> by HENMODEL:def 1;
consider y being bound_QC-variable of Al such that
A4: X |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A1;
consider f2 being FinSequence of CQC-WFF Al such that
A5: rng f2 c= X and
A6: |- f2 ^ <*(('not' (Ex (x,p))) 'or' (p . (x,y)))*> by A4, HENMODEL:def 1;
take y ; :: thesis:
A7: |- (f1 ^ f2) ^ <*(Ex (x,p))*> by A3, HENMODEL:5;
|- (f1 ^ f2) ^ <*(('not' (Ex (x,p))) 'or' (p . (x,y)))*> by A6, CALCUL_2:20;
then A8: |- (f1 ^ f2) ^ <*(p . (x,y))*> by A7, Th2;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then rng (f1 ^ f2) c= X by A2, A5, XBOOLE_1:8;
hence X |- p . (x,y) by A8, HENMODEL:def 1; :: thesis:

end;

thus ( ex y being bound_QC-variable of Al st X |- p . (x,y) implies X |- Ex (x,p) ) :: thesis:

proof

given y being bound_QC-variable of Al such that A9: X |- p . (x,y) ; :: thesis:
consider f1 being FinSequence of CQC-WFF Al such that
A10: rng f1 c= X and
A11: |- f1 ^ <*(p . (x,y))*> by A9, HENMODEL:def 1;
|- f1 ^ <*(Ex (x,p))*> by A11, CALCUL_1:58;
hence X |- Ex (x,p) by A10, HENMODEL:def 1; :: thesis:

end;