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

proof

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

end;

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

proof

given y being bound_QC-variable such that A6: X |- p . x,y ; :: thesis: X |- Ex x,p
consider f1 being FinSequence of CQC-WFF such that
A7: ( rng f1 c= X & |- f1 ^ <*(p . x,y)*> ) by A6, HENMODEL:def 2;
|- f1 ^ <*(Ex x,p)*> by A7, CALCUL_1:58;
hence X |- Ex x,p by A7, HENMODEL:def 2; :: thesis: verum

end;