let G be _Graph; :: thesis: for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
G .reachableFrom v1 = G .reachableFrom v2
let v1, v2 be Vertex of G; :: thesis: ( v1 in G .reachableFrom v2 implies G .reachableFrom v1 = G .reachableFrom v2 )
assume v1 in G .reachableFrom v2 ; :: thesis: G .reachableFrom v1 = G .reachableFrom v2
then consider WA being Walk of G such that
A1: WA is_Walk_from v2,v1 by Def5;
A2: WA .reverse() is_Walk_from v1,v2 by A1, GLIB_001:23;

now :: thesis: for x being object holds
( ( x in G .reachableFrom v1 implies x in G .reachableFrom v2 ) & ( x in G .reachableFrom v2 implies x in G .reachableFrom v1 ) )

let x be object ; :: thesis: ( ( x in G .reachableFrom v1 implies x in G .reachableFrom v2 ) & ( x in G .reachableFrom v2 implies x in G .reachableFrom v1 ) )

hereby :: thesis: ( x in G .reachableFrom v2 implies x in G .reachableFrom v1 )

assume x in G .reachableFrom v1 ; :: thesis: x in G .reachableFrom v2
then consider WB being Walk of G such that
A3: WB is_Walk_from v1,x by Def5;
WA .append WB is_Walk_from v2,x by A1, A3, GLIB_001:31;
hence x in G .reachableFrom v2 by Def5; :: thesis: verum

end;

assume x in G .reachableFrom v2 ; :: thesis: x in G .reachableFrom v1
then consider WB being Walk of G such that
A4: WB is_Walk_from v2,x by Def5;
(WA .reverse()) .append WB is_Walk_from v1,x by A2, A4, GLIB_001:31;
hence x in G .reachableFrom v1 by Def5; :: thesis: verum

end;

hence G .reachableFrom v1 = G .reachableFrom v2 by TARSKI:2; :: thesis: verum