[STATEMENT]
lemma arev_in_arcs[simp]: "a \<in> arcs G \<Longrightarrow> arev a \<in> arcs G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> arcs G \<Longrightarrow> arev a \<in> arcs G
[PROOF STEP]
by (metis arev_arev arev_dom)