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() by Def36; :: 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, Def36; :: 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, Def36;
A3: the_Target_of G1 = the_Target_of G2 by A1, Def36;

A4: now

let e be set ; :: 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, Def28;
hence ( e in G1 .edgesInto X iff e in G2 .edgesInto X ) by Def28; :: 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, Def36;

A7: now

let e be set ; :: 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, Def29;
hence ( e in G1 .edgesOutOf X iff e in G2 .edgesOutOf X ) by Def29; :: 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

let e be set ; :: 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 Def33;
then ( e in G1 .edgesDBetween X,Y iff e DSJoins X,Y,G2 ) by A1, Th91;
hence ( e in G2 .edgesDBetween X,Y iff e in G1 .edgesDBetween X,Y ) by Def33; :: thesis: verum

end;

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