[STATEMENT]
lemma fdomainI[intro]: 
  assumes "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r"
  shows "a \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r
[PROOF STEP]
unfolding fdomain_def
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> set {a. \<exists>b. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r}
[PROOF STEP]
by auto