let G1, G2 be _Graph; :: thesis: for X, Y being set st G1 == G2 holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )
let X, Y be set ; :: thesis: ( G1 == G2 implies ( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) ) )
assume A1: G1 == G2 ; :: thesis: ( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )
hence G1 .order() = G2 .order() ; :: thesis: ( G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )
thus G1 .size() = G2 .size() by A1; :: thesis: ( G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )
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: for e being object holds
( e in G1 .edgesInto X iff e in G2 .edgesInto X )

let e be object ; :: thesis: ( e in G1 .edgesInto X iff e in G2 .edgesInto X )
( 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: verum

end;

hence A5: G1 .edgesInto X = G2 .edgesInto X by TARSKI:2; :: thesis: ( G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )
A6: the_Source_of G1 = the_Source_of G2 by A1;

A7: now :: thesis: for e being object holds
( e in G1 .edgesOutOf X iff e in G2 .edgesOutOf X )

let e be object ; :: thesis: ( e in G1 .edgesOutOf X iff e in G2 .edgesOutOf X )
( 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: verum

end;

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

now :: thesis: for e being object holds
( e in G2 .edgesDBetween (X,Y) iff e in G1 .edgesDBetween (X,Y) )

let e be object ; :: thesis: ( e in G2 .edgesDBetween (X,Y) iff e in G1 .edgesDBetween (X,Y) )
( 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: verum

end;

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