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

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

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

then A5:
G1 .reachableFrom v1 c= G2 .reachableFrom v2
by TARSKI:def 3;
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;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

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