let G1 be _Graph; :: thesis: for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) holds
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let G2 be Subgraph of G1; :: thesis: ( ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) implies for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 )
assume A1: for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ; :: 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 A2: v1 = v2 ; :: thesis: G1 .reachableFrom v1 = G2 .reachableFrom v2
for w being object st w in G1 .reachableFrom v1 holds
w in G2 .reachableFrom v2
proof
let w be object ; :: thesis: ( w in G1 .reachableFrom v1 implies w in G2 .reachableFrom v2 )
assume w in G1 .reachableFrom v1 ; :: thesis: w in G2 .reachableFrom v2
then consider W1 being Walk of G1 such that
A3: W1 is_Walk_from v1,w by GLIB_002:def 5;
( W1 .first() = v1 & W1 .last() = w ) by A3, GLIB_001:def 23;
then consider W2 being Walk of G2 such that
A4: W2 is_Walk_from v1,w by A1;
thus w in G2 .reachableFrom v2 by A2, A4, GLIB_002:def 5; :: thesis: verum
end;
then A5: G1 .reachableFrom v1 c= G2 .reachableFrom v2 by TARSKI:def 3;
G2 .reachableFrom v2 c= G1 .reachableFrom v1 by A2, GLIB_002:14;
hence G1 .reachableFrom v1 = G2 .reachableFrom v2 by A5, XBOOLE_0:def 10; :: thesis: verum