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 GLIB_000:def 31;
then e SJoins X,Y,G by GLIB_009:11;
hence e in G .edgesBetween (X,Y) by GLIB_000:def 30; :: thesis: verum
end;
hence G .edgesDBetween (X,Y) c= G .edgesBetween (X,Y) by TARSKI:def 3; :: thesis: verum