let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies G1 .reachableFrom v1 = G2 .reachableFrom v2 )
assume A1: v1 = v2 ; :: thesis: G1 .reachableFrom v1 = G2 .reachableFrom v2
for v being object holds
( v in G1 .reachableFrom v1 iff v in G2 .reachableFrom v2 )

proof

let v be object ; :: thesis: ( v in G1 .reachableFrom v1 iff v in G2 .reachableFrom v2 )

hereby :: thesis: ( v in G2 .reachableFrom v2 implies v in G1 .reachableFrom v1 )

assume v in G1 .reachableFrom v1 ; :: thesis: v in G2 .reachableFrom v2
then ex W being Walk of G1 st W is_Walk_from v1,v by GLIB_002:def 5;
then ex W being Walk of G2 st W is_Walk_from v2,v by A1, Th19;
hence v in G2 .reachableFrom v2 by GLIB_002:def 5; :: thesis: verum

end;

assume v in G2 .reachableFrom v2 ; :: thesis: v in G1 .reachableFrom v1
then ex W being Walk of G2 st W is_Walk_from v2,v by GLIB_002:def 5;
then ex W being Walk of G1 st W is_Walk_from v1,v by A1, Th19;
hence v in G1 .reachableFrom v1 by GLIB_002:def 5; :: thesis: verum

end;

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