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

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

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

end;

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