let G1, G2 be _Graph; :: thesis:
let X, Y be set ; :: thesis:
assume A1: G1 == G2 ; :: thesis:
hence G1 .order() = G2 .order() ; :: thesis:
thus G1 .size() = G2 .size() by A1; :: thesis:
A2: the_Edges_of G1 = the_Edges_of G2 by A1;
A3: the_Target_of G1 = the_Target_of G2 by A1;

A4: now :: thesis:

let e be object ; :: thesis:
( e in G1 .edgesInto X iff ( e in the_Edges_of G2 & (the_Target_of G2) . e in X ) ) by A2, A3, Def26;
hence ( e in G1 .edgesInto X iff e in G2 .edgesInto X ) by Def26; :: thesis:

end;

hence A5: G1 .edgesInto X = G2 .edgesInto X by TARSKI:2; :: thesis:
A6: the_Source_of G1 = the_Source_of G2 by A1;

A7: now :: thesis:

let e be object ; :: thesis:
( e in G1 .edgesOutOf X iff ( e in the_Edges_of G2 & (the_Source_of G2) . e in X ) ) by A2, A6, Def27;
hence ( e in G1 .edgesOutOf X iff e in G2 .edgesOutOf X ) by Def27; :: thesis:

end;

hence A8: G1 .edgesOutOf X = G2 .edgesOutOf X by TARSKI:2; :: thesis:
thus G1 .edgesInOut X = G2 .edgesInOut X by A5, A7, TARSKI:2; :: thesis:
thus G1 .edgesBetween X = G2 .edgesBetween X by A4, A8, TARSKI:2; :: thesis:

now :: thesis:

let e be object ; :: thesis:
( e in G1 .edgesDBetween (X,Y) iff e DSJoins X,Y,G1 ) by Def31;
then ( e in G1 .edgesDBetween (X,Y) iff e DSJoins X,Y,G2 ) by A1;
hence ( e in G2 .edgesDBetween (X,Y) iff e in G1 .edgesDBetween (X,Y) ) by Def31; :: thesis:

end;

hence G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) by TARSKI:2; :: thesis: