[STATEMENT]
lemma subgraph_subset:
  assumes "subgraph G\<^sub>1 G\<^sub>2"
  shows "vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2" "edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
 2. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
have vrt:"Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2"
    and ep:"edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgraph G\<^sub>1 G\<^sub>2

goal (1 subgoal):
 1. Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices G\<^sub>1 = Domain (Id_on (vertices G\<^sub>1)) \<and> graph G\<^sub>1 \<and> graph G\<^sub>2 \<and> Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 \<and> univalent (Id_on (vertices G\<^sub>1)) \<and> edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)

goal (1 subgoal):
 1. Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)

goal (2 subgoals):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
 2. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
hence "edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)

goal (1 subgoal):
 1. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
subgraph G\<^sub>1 G\<^sub>2

goal (1 subgoal):
 1. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
unfolding edge_preserving
[PROOF STATE]
proof (prove)
using this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
on_triple (Id_on (vertices G\<^sub>1)) `` edges G\<^sub>1 \<subseteq> edges G\<^sub>2
subgraph G\<^sub>1 G\<^sub>2

goal (1 subgoal):
 1. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2

goal (2 subgoals):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
 2. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
thus "vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2" "edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2

goal (1 subgoal):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
using vrt
[PROOF STATE]
proof (prove)
using this:
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2

goal (1 subgoal):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed