let p be Element of CQC-WFF ; :: thesis:
let x be bound_QC-variable; :: thesis:
let CX be Consistent Subset of CQC-WFF ; :: thesis:
let JH be Henkin_interpretation of CX; :: thesis:
thus ( JH, valH |= Ex x,p implies ex y being bound_QC-variable st JH, valH |= p . x,y ) :: thesis:

proof

assume JH, valH |= Ex x,p ; :: thesis:
then consider x1 being Element of HCar such that
A1: JH,valH . (x | x1) |= p by Th9;
( rng valH = bound_QC-variables & dom valH = bound_QC-variables ) by HENMODEL:def 7, RELAT_1:71;
then consider b being set such that
A2: ( b in dom valH & valH . b = x1 ) by FUNCT_1:def 5, HENMODEL:def 5;
reconsider y = b as bound_QC-variable by A2;
take y ; :: thesis:
thus JH, valH |= p . x,y by A1, A2, CALCUL_1:24; :: thesis:

end;

thus ( ex y being bound_QC-variable st JH, valH |= p . x,y implies JH, valH |= Ex x,p ) :: thesis:

proof

given y being bound_QC-variable such that A3: JH, valH |= p . x,y ; :: thesis:
consider x1 being Element of HCar such that
A4: ( valH . y = x1 & JH,valH . (x | x1) |= p ) by A3, CALCUL_1:24;
thus JH, valH |= Ex x,p by A4, Th9; :: thesis:

end;