let G be _Graph; :: thesis: for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
v2 in G .reachableFrom v1
let v1, v2 be Vertex of G; :: thesis: ( v1 in G .reachableFrom v2 implies v2 in G .reachableFrom v1 )
assume v1 in G .reachableFrom v2 ; :: thesis: v2 in G .reachableFrom v1
then G .reachableFrom v2 = G .reachableFrom v1 by GLIB_002:12;
hence v2 in G .reachableFrom v1 by GLIB_002:9; :: thesis: verum