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 e Joins x,y,G ; :: thesis: ( e DJoins x,y,G or e DJoins y,x,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 DJoins x,y,G or e DJoins y,x,G ) by Def16; :: thesis: verum

end;

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