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

now :: thesis: for e being object st e in G .edgesDBetween (X,Y) holds
e in G .edgesBetween (X,Y)

let e be object ; :: thesis: ( e in G .edgesDBetween (X,Y) implies e in G .edgesBetween (X,Y) )
assume e in G .edgesDBetween (X,Y) ; :: thesis: e in G .edgesBetween (X,Y)
then e DSJoins X,Y,G by Def31;
then e SJoins X,Y,G ;
hence e in G .edgesBetween (X,Y) by Def30; :: thesis: verum

end;

hence G .edgesDBetween (X,Y) c= G .edgesBetween (X,Y) ; :: thesis: verum