let G1, G2 be _Graph; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume that
A1: G1 == G2 and
A2: v1 = v2 ; :: thesis:

assume x in G1 .reachableFrom v1 ; :: thesis:
then consider W being Walk of G1 such that
A3: W is_Walk_from v2,x by A2, Def5;
reconsider W2 = W as Walk of G2 by A1, GLIB_001:179;
W2 is_Walk_from v2,x by A3, GLIB_001:19;
hence x in G2 .reachableFrom v2 by Def5; :: thesis:

end;

assume x in G2 .reachableFrom v2 ; :: thesis:
then consider W being Walk of G2 such that
A4: W is_Walk_from v1,x by A2, Def5;
reconsider W2 = W as Walk of G1 by A1, GLIB_001:179;
W2 is_Walk_from v1,x by A4, GLIB_001:19;
hence x in G1 .reachableFrom v1 by Def5; :: thesis:

end;