let G be _Graph; :: thesis: for e, x, y, X, Y being set st e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) holds
e SJoins X,Y,G
let e, x, y, X, Y be set ; :: thesis: ( e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) implies e SJoins X,Y,G )
assume that
A1: e Joins x,y,G and
A2: ( ( x in X & y in Y ) or ( x in Y & y in X ) ) ; :: thesis: e SJoins X,Y,G
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 A1, Def15;
e in the_Edges_of G by A1, Def15;
hence e SJoins X,Y,G by A2, A3, Def17; :: thesis: verum