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;

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 ) )

hence
G .reachableFrom v1 = G .reachableFrom v2
by TARSKI:2; :: thesis: verum( ( 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 ) )

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;hereby :: thesis: ( x in G .reachableFrom v2 implies x in G .reachableFrom v1 )

assume
x in G .reachableFrom v2
; :: thesis: x in G .reachableFrom v1assume
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;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

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