[STATEMENT]
lemma distinct_vertices12[simp]: "vertex_1 \<noteq> vertex_2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex_1 \<noteq> vertex_2
[PROOF STEP]
using distinct_vertices
[PROOF STATE]
proof (prove)
using this:
distinct [vertex_1, vertex_2, vertex_3]

goal (1 subgoal):
 1. vertex_1 \<noteq> vertex_2
[PROOF STEP]
by(simp)