[STATEMENT]
lemma connected_verts_G_eq_T:
  assumes "graph G" and "connected G"
  shows "verts T = verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
have "root \<in> verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root \<in> verts G
[PROOF STEP]
using root_in_G
[PROOF STATE]
proof (prove)
using this:
root \<in> verts G

goal (1 subgoal):
 1. root \<in> verts G
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
root \<in> verts G

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
root \<in> verts G
[PROOF STEP]
have "\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x"
[PROOF STATE]
proof (prove)
using this:
root \<in> verts G

goal (1 subgoal):
 1. \<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
[PROOF STEP]
using graph.connected_iff_reachable assms(1,2)
[PROOF STATE]
proof (prove)
using this:
root \<in> verts G
graph ?G \<Longrightarrow> Digraph_Component.connected ?G = ((\<forall>x\<in>verts ?G. \<forall>y\<in>verts ?G. x \<rightarrow>\<^sup>*\<^bsub>?G\<^esub> y) \<and> verts ?G \<noteq> {})
graph G
Digraph_Component.connected G

goal (1 subgoal):
 1. \<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
using reachable_verts_G_eq_T
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x
\<forall>x\<in>verts G. root \<rightarrow>\<^sup>*\<^bsub>G\<^esub> x \<Longrightarrow> verts T = verts G

goal (1 subgoal):
 1. verts T = verts G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
verts T = verts G

goal:
No subgoals!
[PROOF STEP]
qed