let G be _Graph; :: thesis: for e being set
for v being Vertex of G holds
( e in v .edgesInOut() iff e Joins v,v .adj e,G )
let e be set ; :: thesis: for v being Vertex of G holds
( e in v .edgesInOut() iff e Joins v,v .adj e,G )
let v be Vertex of G; :: thesis: ( e in v .edgesInOut() iff e Joins v,v .adj e,G )

hereby :: thesis: ( e Joins v,v .adj e,G implies e in v .edgesInOut() )

assume A1: e in v .edgesInOut() ; :: thesis: e Joins v,v .adj e,G
then A2: ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by Th61;

now :: thesis: e Joins v,v .adj e,G

per cases ( (the_Target_of G) . e = v or (the_Target_of G) . e <> v ) ;

suppose A3: (the_Target_of G) . e = v ; :: thesis: e Joins v,v .adj e,G

then v .adj e = (the_Source_of G) . e by A1, Def41;
hence e Joins v,v .adj e,G by A1, A3, Def13; :: thesis: verum

end;

suppose A4: (the_Target_of G) . e <> v ; :: thesis: e Joins v,v .adj e,G

then v .adj e = (the_Target_of G) . e by A1, A2, Def41;
hence e Joins v,v .adj e,G by A1, A2, A4, Def13; :: thesis: verum

end;

end;

end;

hence e Joins v,v .adj e,G ; :: thesis: verum

end;

assume e Joins v,v .adj e,G ; :: thesis: e in v .edgesInOut()
hence e in v .edgesInOut() by Th62; :: thesis: verum