let G be _Graph; :: thesis: for x, X, y, e being set st x in X & y in X & e Joins x,y,G holds
e in G .edgesBetween X
let x, X, y, e be set ; :: thesis: ( x in X & y in X & e Joins x,y,G implies e in G .edgesBetween X )
assume that
A1: ( x in X & y in X ) and
A2: e Joins x,y,G ; :: thesis: e in G .edgesBetween X
A3: ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) by A2, Def15;
e in the_Edges_of G by A2, Def15;
hence e in G .edgesBetween X by A1, A3, Lm6; :: thesis: verum