let G be _Graph; :: thesis: for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) )
let e, x, y be set ; :: thesis: ( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) )

hereby :: thesis: ( ( e DJoins x,y,G or e DJoins y,x,G ) implies e Joins x,y,G )

assume A1: e Joins x,y,G ; :: thesis: ( e DJoins x,y,G or e DJoins y,x,G )
then A2: ( ( (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;
e in the_Edges_of G by A1, Def15;
hence ( e DJoins x,y,G or e DJoins y,x,G ) by A2, Def16; :: thesis: verum

end;

assume A3: ( e DJoins x,y,G or e DJoins y,x,G ) ; :: thesis: e Joins x,y,G
then A4: ( ( (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 Def16;
e in the_Edges_of G by A3, Def16;
hence e Joins x,y,G by A4, Def15; :: thesis: verum