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)

now :: thesis: for e being object holds
( 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 Def30;
then ( e in G .edgesBetween (X,Y) iff e SJoins Y,X,G ) ;
hence ( e in G .edgesBetween (X,Y) iff e in G .edgesBetween (Y,X) ) by Def30; :: thesis: verum

end;

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