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:
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 ;
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 ;
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 ;
hence x in G .reachableFrom v1 by Def5; :: thesis: verum
end;
hence G .reachableFrom v1 = G .reachableFrom v2 by TARSKI:2; :: thesis: verum