let G be _Graph; :: thesis: for e, x, y being set st e Joins x,y,G holds
e Joins y,x,G
let e, x, y be set ; :: thesis: ( e Joins x,y,G implies e Joins y,x,G )
assume A1: e Joins x,y,G ; :: thesis: e Joins 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 Joins y,x,G by A2, Def15; :: thesis: verum