# [isabelle] A proof for existential

Hi all,

`I've been stuck trying to find a proof for the following, could someone
``please shed some light?
`
axiomatization
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y => hx > h y" and
ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"
lemma "EX x. gx = 0"
oops
I've tried:
lemma "EX x. gx = 0"
using ax1 ax2
apply (intro exI)
apply (erule exE)+
apply (erule allE)
apply (erule impE)
which gives 2 subgoals, but they don't seem to be in the right direction...
Thanks for the help in advance.
Thanks
John

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*