[STATEMENT]
lemma (in Network) am_s_is_incoming:
  assumes "is_adj_map am"
  shows "E``{s} = set (am s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` {s} = set (am s)
[PROOF STEP]
using assms no_incoming_s
[PROOF STATE]
proof (prove)
using this:
is_adj_map am
\<forall>u. (u, s) \<notin> E

goal (1 subgoal):
 1. E `` {s} = set (am s)
[PROOF STEP]
unfolding is_adj_map_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u. distinct (am u) \<and> set (am u) = E `` {u} \<union> E\<inverse> `` {u}
\<forall>u. (u, s) \<notin> E

goal (1 subgoal):
 1. E `` {s} = set (am s)
[PROOF STEP]
by auto