let G1, G2 be _Graph; 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 ; ( 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
; ( 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()
; ( 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; ( 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;
hence A5:
G1 .edgesInto X = G2 .edgesInto X
by TARSKI:2; ( 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;
hence A8:
G1 .edgesOutOf X = G2 .edgesOutOf X
by TARSKI:2; ( 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; ( 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; G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y)
now for e being object holds
( e in G2 .edgesDBetween (X,Y) iff e in G1 .edgesDBetween (X,Y) )let e be
object ;
( 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;
verum end;
hence
G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y)
by TARSKI:2; verum