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 Def30;
then ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) ;
hence e in G .edgesBetween X by Lm5; :: 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 Lm5;
then e SJoins X,X,G ;
hence e in G .edgesBetween (X,X) by Def30; :: thesis: verum

end;

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