let G be _Graph; :: thesis: for v being Vertex of G
for e being set holds
( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) )
let v be Vertex of G; :: thesis: for e being set holds
( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) )
let e be set ; :: thesis: ( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) )

hereby :: thesis: ( e in the_Edges_of G & (the_Target_of G) . e = v implies e in v .edgesIn() )

assume A1: e in v .edgesIn() ; :: thesis: ( e in the_Edges_of G & (the_Target_of G) . e = v )
then (the_Target_of G) . e in {v} by Def26;
hence ( e in the_Edges_of G & (the_Target_of G) . e = v ) by A1, TARSKI:def 1; :: thesis: verum

end;

assume that
A2: e in the_Edges_of G and
A3: (the_Target_of G) . e = v ; :: thesis: e in v .edgesIn()
(the_Target_of G) . e in {v} by A3, TARSKI:def 1;
hence e in v .edgesIn() by A2, Def26; :: thesis: verum