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

proof

assume JH, valH |= Ex (x,p) ; :: thesis: ex y being bound_QC-variable st JH, valH |= p . (x,y)
then consider x1 being Element of HCar such that
A1: JH,valH . (x | x1) |= p by Th9;
rng valH = bound_QC-variables by HENMODEL:def 6, RELAT_1:45;
then consider b being set such that
A2: b in dom valH and
A3: valH . b = x1 by FUNCT_1:def 3, HENMODEL:def 4;
reconsider y = b as bound_QC-variable by A2;
take y ; :: thesis: JH, valH |= p . (x,y)
thus JH, valH |= p . (x,y) by A1, A3, CALCUL_1:24; :: thesis: verum

end;

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

proof

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

end;