let G1, G2 be _Graph; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableDFrom v1 = G2 .reachableDFrom v2

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableDFrom v1 = G2 .reachableDFrom v2

let v2 be Vertex of G2; :: thesis: ( G1 == G2 & v1 = v2 implies G1 .reachableDFrom v1 = G2 .reachableDFrom v2 )

assume that

A1: G1 == G2 and

A2: v1 = v2 ; :: thesis: G1 .reachableDFrom v1 = G2 .reachableDFrom v2

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableDFrom v1 = G2 .reachableDFrom v2

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableDFrom v1 = G2 .reachableDFrom v2

let v2 be Vertex of G2; :: thesis: ( G1 == G2 & v1 = v2 implies G1 .reachableDFrom v1 = G2 .reachableDFrom v2 )

assume that

A1: G1 == G2 and

A2: v1 = v2 ; :: thesis: G1 .reachableDFrom v1 = G2 .reachableDFrom v2

now :: thesis: for x being object holds

( ( x in G1 .reachableDFrom v1 implies x in G2 .reachableDFrom v2 ) & ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 ) )

hence
G1 .reachableDFrom v1 = G2 .reachableDFrom v2
by TARSKI:2; :: thesis: verum( ( x in G1 .reachableDFrom v1 implies x in G2 .reachableDFrom v2 ) & ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 ) )

let x be object ; :: thesis: ( ( x in G1 .reachableDFrom v1 implies x in G2 .reachableDFrom v2 ) & ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 ) )

then consider W being DWalk of G2 such that

A4: W is_Walk_from v1,x by A2, Def6;

reconsider W2 = W as DWalk of G1 by A1, GLIB_001:179, GLIB_001:181;

W2 is_Walk_from v1,x by A4, GLIB_001:19;

hence x in G1 .reachableDFrom v1 by Def6; :: thesis: verum

end;hereby :: thesis: ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 )

assume
x in G2 .reachableDFrom v2
; :: thesis: x in G1 .reachableDFrom v1assume
x in G1 .reachableDFrom v1
; :: thesis: x in G2 .reachableDFrom v2

then consider W being DWalk of G1 such that

A3: W is_Walk_from v2,x by A2, Def6;

reconsider W2 = W as DWalk of G2 by A1, GLIB_001:179, GLIB_001:181;

W2 is_Walk_from v2,x by A3, GLIB_001:19;

hence x in G2 .reachableDFrom v2 by Def6; :: thesis: verum

end;then consider W being DWalk of G1 such that

A3: W is_Walk_from v2,x by A2, Def6;

reconsider W2 = W as DWalk of G2 by A1, GLIB_001:179, GLIB_001:181;

W2 is_Walk_from v2,x by A3, GLIB_001:19;

hence x in G2 .reachableDFrom v2 by Def6; :: thesis: verum

then consider W being DWalk of G2 such that

A4: W is_Walk_from v1,x by A2, Def6;

reconsider W2 = W as DWalk of G1 by A1, GLIB_001:179, GLIB_001:181;

W2 is_Walk_from v1,x by A4, GLIB_001:19;

hence x in G1 .reachableDFrom v1 by Def6; :: thesis: verum