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

now :: thesis: for e being object holds
( ( e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) implies e SJoins X,Y,G ) & ( e SJoins X,Y,G implies e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) ) )

let e be object ; :: thesis: ( ( e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) implies e SJoins X,Y,G ) & ( e SJoins X,Y,G implies b₁ in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) ) )

hereby :: thesis: ( e SJoins X,Y,G implies b₁ in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) )

assume e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) ; :: thesis: e SJoins X,Y,G

per cases then ( e in G .edgesDBetween (X,Y) or e in G .edgesDBetween (Y,X) ) by XBOOLE_0:def 3;

suppose e in G .edgesDBetween (X,Y) ; :: thesis: e SJoins X,Y,G

then e DSJoins X,Y,G by Def31;
hence e SJoins X,Y,G ; :: thesis: verum

end;

suppose e in G .edgesDBetween (Y,X) ; :: thesis: e SJoins X,Y,G

then e DSJoins Y,X,G by Def31;
hence e SJoins X,Y,G ; :: thesis: verum

end;

end;

end;

assume e SJoins X,Y,G ; :: thesis: b₁ in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X))

per cases then ( e DSJoins X,Y,G or e DSJoins Y,X,G ) ;

suppose e DSJoins X,Y,G ; :: thesis: b₁ in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X))

then e in G .edgesDBetween (X,Y) by Def31;
hence e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose e DSJoins Y,X,G ; :: thesis: b₁ in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X))

then e in G .edgesDBetween (Y,X) by Def31;
hence e in (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence G .edgesBetween (X,Y) = (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X)) by Def30; :: thesis: verum