let G be _Graph; :: thesis: for e being set
for v1 being Vertex of G holds
( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G )
let e be set ; :: thesis: for v1 being Vertex of G holds
( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G )
let v1 be Vertex of G; :: thesis: ( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G )

hereby :: thesis: ( ex v2 being Vertex of G st e Joins v1,v2,G implies e in v1 .edgesInOut() )

assume A1: e in v1 .edgesInOut() ; :: thesis: ex v2 being Vertex of G st e Joins v1,v2,G

now

per cases ( (the_Source_of G) . e = v1 or (the_Target_of G) . e = v1 ) by A1, Th64;

suppose A2: (the_Source_of G) . e = v1 ; :: thesis: ex v2 being Vertex of G st e Joins v1,v2,G

set v2 = (the_Target_of G) . e;
reconsider v2 = (the_Target_of G) . e as Vertex of G by A1, FUNCT_2:5;
take v2 = v2; :: thesis: e Joins v1,v2,G
thus e Joins v1,v2,G by A1, A2, Def15; :: thesis: verum

end;

suppose A3: (the_Target_of G) . e = v1 ; :: thesis: ex v2 being Vertex of G st e Joins v1,v2,G

set v2 = (the_Source_of G) . e;
reconsider v2 = (the_Source_of G) . e as Vertex of G by A1, FUNCT_2:5;
take v2 = v2; :: thesis: e Joins v1,v2,G
thus e Joins v1,v2,G by A1, A3, Def15; :: thesis: verum

end;

end;

end;

hence ex v2 being Vertex of G st e Joins v1,v2,G ; :: thesis: verum

end;

given v2 being Vertex of G such that A4: e Joins v1,v2,G ; :: thesis: e in v1 .edgesInOut()
thus e in v1 .edgesInOut() by A4, Th65; :: thesis: verum