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)

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) )

hence
G .edgesBetween (X,X) = G .edgesDBetween (X,X)
by TARSKI:2; :: thesis: verum( 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 GLIB_000:def 30;

then ( e in G .edgesBetween (X,X) iff e DSJoins X,X,G ) by Th11;

hence ( e in G .edgesBetween (X,X) iff e in G .edgesDBetween (X,X) ) by GLIB_000:def 31; :: thesis: verum

end;( e in G .edgesBetween (X,X) iff e SJoins X,X,G ) by GLIB_000:def 30;

then ( e in G .edgesBetween (X,X) iff e DSJoins X,X,G ) by Th11;

hence ( e in G .edgesBetween (X,X) iff e in G .edgesDBetween (X,X) ) by GLIB_000:def 31; :: thesis: verum