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 .reachableFrom v1 = G2 .reachableFrom v2

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

let v2 be Vertex of G2; :: thesis: ( G1 == G2 & v1 = v2 implies G1 .reachableFrom v1 = G2 .reachableFrom v2 )
assume that
A1: G1 == G2 and
A2: v1 = v2 ; :: thesis: G1 .reachableFrom v1 = G2 .reachableFrom v2
now :: thesis: for x being object holds
( ( x in G1 .reachableFrom v1 implies x in G2 .reachableFrom v2 ) & ( x in G2 .reachableFrom v2 implies x in G1 .reachableFrom v1 ) )
let x be object ; :: thesis: ( ( x in G1 .reachableFrom v1 implies x in G2 .reachableFrom v2 ) & ( x in G2 .reachableFrom v2 implies x in G1 .reachableFrom v1 ) )
hereby :: thesis: ( x in G2 .reachableFrom v2 implies x in G1 .reachableFrom v1 )
assume x in G1 .reachableFrom v1 ; :: thesis: x in G2 .reachableFrom v2
then consider W being Walk of G1 such that
A3: W is_Walk_from v2,x by ;
reconsider W2 = W as Walk of G2 by ;
W2 is_Walk_from v2,x by ;
hence x in G2 .reachableFrom v2 by Def5; :: thesis: verum
end;
assume x in G2 .reachableFrom v2 ; :: thesis: x in G1 .reachableFrom v1
then consider W being Walk of G2 such that
A4: W is_Walk_from v1,x by ;
reconsider W2 = W as Walk of G1 by ;
W2 is_Walk_from v1,x by ;
hence x in G1 .reachableFrom v1 by Def5; :: thesis: verum
end;
hence G1 .reachableFrom v1 = G2 .reachableFrom v2 by TARSKI:2; :: thesis: verum