let G1, G2 be _Graph; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableDFrom v1 = G2 .reachableDFrom v2
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableDFrom v1 = G2 .reachableDFrom v2
let v2 be Vertex of G2; :: thesis: ( G1 == G2 & v1 = v2 implies G1 .reachableDFrom v1 = G2 .reachableDFrom v2 )
assume that
A1: G1 == G2 and
A2: v1 = v2 ; :: thesis: G1 .reachableDFrom v1 = G2 .reachableDFrom v2
now :: thesis: for x being object holds
( ( x in G1 .reachableDFrom v1 implies x in G2 .reachableDFrom v2 ) & ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 ) )
let x be object ; :: thesis: ( ( x in G1 .reachableDFrom v1 implies x in G2 .reachableDFrom v2 ) & ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 ) )
hereby :: thesis: ( x in G2 .reachableDFrom v2 implies x in G1 .reachableDFrom v1 )
assume x in G1 .reachableDFrom v1 ; :: thesis: x in G2 .reachableDFrom v2
then consider W being DWalk of G1 such that
A3: W is_Walk_from v2,x by A2, Def6;
reconsider W2 = W as DWalk of G2 by A1, GLIB_001:179, GLIB_001:181;
W2 is_Walk_from v2,x by A3, GLIB_001:19;
hence x in G2 .reachableDFrom v2 by Def6; :: thesis: verum
end;
assume x in G2 .reachableDFrom v2 ; :: thesis: x in G1 .reachableDFrom v1
then consider W being DWalk of G2 such that
A4: W is_Walk_from v1,x by A2, Def6;
reconsider W2 = W as DWalk of G1 by A1, GLIB_001:179, GLIB_001:181;
W2 is_Walk_from v1,x by A4, GLIB_001:19;
hence x in G1 .reachableDFrom v1 by Def6; :: thesis: verum
end;
hence G1 .reachableDFrom v1 = G2 .reachableDFrom v2 by TARSKI:2; :: thesis: verum