theory John imports Complex_Main
begin

axiomatization
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y --> h x > h y" and
ax2: "ALL x. (ALL y. x ~= y --> h x > h y) --> g x = 0"

lemma "EX x. g x = 0"
by (metis ax1 ax2)

lemma "EX x. g x = 0"
 apply (insert ax1)
 apply (erule exE)
 apply (rule_tac x="x" in exI)
 apply (erule_tac ax2[THEN spec, THEN mp])
done

lemma "EX x. g x = 0"
proof -
  from ax1 obtain x where A: "ALL y. x ~= y --> h y < h x" ..
  from ax2 have "(ALL y. x ~= y --> h x > h y) --> g x = 0" ..
  hence "g x = 0" using A ..
  thus "EX x. g x = 0" ..
qed

end