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 :: thesis: ex v2 being Vertex of G st e Joins v1,v2,G
per cases ( (the_Source_of G) . e = v1 or (the_Target_of G) . e = v1 ) by A1, Th61;
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; :: 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; :: 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, Th62; :: thesis: verum