[STATEMENT]
lemma subgraph_trans: 
  assumes "graph_system V E"
  assumes "graph_system V' E'"
  assumes "graph_system V'' E''"
  shows "subgraph V'' E'' V' E' \<Longrightarrow> subgraph V' E' V E \<Longrightarrow> subgraph V'' E'' V E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>subgraph V'' E'' V' E'; subgraph V' E' V E\<rbrakk> \<Longrightarrow> subgraph V'' E'' V E
[PROOF STEP]
by (meson assms(1) assms(3) is_subgraphI subgraph.edges_ss subgraph.verts_ss subset_trans)