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

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

let e be object ; :: thesis: ( ( e in G .edgesBetween (X,X) implies e in G .edgesBetween X ) & ( e in G .edgesBetween X implies e in G .edgesBetween (X,X) ) )

hereby :: thesis: ( e in G .edgesBetween X implies e in G .edgesBetween (X,X) )

assume e in G .edgesBetween (X,X) ; :: thesis: e in G .edgesBetween X
then e SJoins X,X,G by GLIB_000:def 30;
then ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) by GLIB_000:def 15;
hence e in G .edgesBetween X by GLIB_000:31; :: thesis: verum

end;

assume e in G .edgesBetween X ; :: thesis: e in G .edgesBetween (X,X)
then ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) by GLIB_000:31;
then e SJoins X,X,G by GLIB_000:def 15;
hence e in G .edgesBetween (X,X) by GLIB_000:def 30; :: thesis: verum

end;

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