[STATEMENT]
lemma betw_b_in_path:
  assumes abc: "[a;b;c]"
      and path_ab: "path ac a c"
  shows "b \<in> ac"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> ac
[PROOF STEP]
using assms abc_ex_path_unique path_unique
[PROOF STATE]
proof (prove)
using this:
[a;b;c]
path ac a c
[?a;?b;?c] \<Longrightarrow> \<exists>!Q. Q \<in> \<P> \<and> ?a \<in> Q \<and> ?b \<in> Q \<and> ?c \<in> Q
\<lbrakk>path ?ab ?a ?b; path ?ab' ?a ?b\<rbrakk> \<Longrightarrow> ?ab = ?ab'

goal (1 subgoal):
 1. b \<in> ac
[PROOF STEP]
by blast