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 A1: ( e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) ) ; :: thesis: e SJoins X,Y,G
then ( e in the_Edges_of G & ( ( (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 Def15;
hence e SJoins X,Y,G by A1, Def17; :: thesis: verum