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 e Joins x,y,G ; :: thesis: e Joins 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 Joins y,x,G by Def15; :: thesis: verum