let G be _Graph; :: thesis: for X, Y being set holds G .edgesBetween (X,Y) = G .edgesBetween (Y,X)

let X, Y be set ; :: thesis: G .edgesBetween (X,Y) = G .edgesBetween (Y,X)

let X, Y be set ; :: thesis: G .edgesBetween (X,Y) = G .edgesBetween (Y,X)

now :: thesis: for e being object holds

( e in G .edgesBetween (X,Y) iff e in G .edgesBetween (Y,X) )

hence
G .edgesBetween (X,Y) = G .edgesBetween (Y,X)
by TARSKI:2; :: thesis: verum( e in G .edgesBetween (X,Y) iff e in G .edgesBetween (Y,X) )

let e be object ; :: thesis: ( e in G .edgesBetween (X,Y) iff e in G .edgesBetween (Y,X) )

( e in G .edgesBetween (X,Y) iff e SJoins X,Y,G ) by GLIB_000:def 30;

then ( e in G .edgesBetween (X,Y) iff e SJoins Y,X,G ) by Th10;

hence ( e in G .edgesBetween (X,Y) iff e in G .edgesBetween (Y,X) ) by GLIB_000:def 30; :: thesis: verum

end;( e in G .edgesBetween (X,Y) iff e SJoins X,Y,G ) by GLIB_000:def 30;

then ( e in G .edgesBetween (X,Y) iff e SJoins Y,X,G ) by Th10;

hence ( e in G .edgesBetween (X,Y) iff e in G .edgesBetween (Y,X) ) by GLIB_000:def 30; :: thesis: verum