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 Def13;
e in the_Edges_of G by A1, Def13;
hence ( e DJoins x,y,G or e DJoins y,x,G ) by A2, Def14; :: 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 Def14;
e in the_Edges_of G by A3, Def14;
hence e Joins x,y,G by A4, Def13; :: thesis: verum