let G be _Graph; :: thesis: for e being object st e in the_Edges_of G holds
e in G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)}
let e be object ; :: thesis: ( e in the_Edges_of G implies e in G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)} )
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
assume A1: e in the_Edges_of G ; :: thesis: e in G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)}
( (the_Source_of G) . e in {((the_Source_of G) . e),((the_Target_of G) . e)} & (the_Target_of G) . e in {((the_Source_of G) . e),((the_Target_of G) . e)} ) by TARSKI:def 2;
hence e in G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)} by A1, Lm5; :: thesis: verum