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 e in v .edgesIn() ; :: thesis: ( e in the_Edges_of G & (the_Target_of G) . e = v )
then ( e in the_Edges_of G & (the_Target_of G) . e in {v} ) by Def28;
hence ( e in the_Edges_of G & (the_Target_of G) . e = v ) by TARSKI:def 1; :: thesis: verum

end;

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