let G1 be _Graph; :: thesis: for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

let G2 be Subgraph of G1; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies G2 .reachableFrom v2 c= G1 .reachableFrom v1 )

assume A1: v1 = v2 ; :: thesis: G2 .reachableFrom v2 c= G1 .reachableFrom v1

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in G2 .reachableFrom v2 or v in G1 .reachableFrom v1 )

assume v in G2 .reachableFrom v2 ; :: thesis: v in G1 .reachableFrom v1

then consider W being Walk of G2 such that

A2: W is_Walk_from v2,v by Def5;

reconsider W2 = W as Walk of G1 by GLIB_001:167;

W2 is_Walk_from v1,v by A1, A2, GLIB_001:19;

hence v in G1 .reachableFrom v1 by Def5; :: thesis: verum

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

let G2 be Subgraph of G1; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies G2 .reachableFrom v2 c= G1 .reachableFrom v1 )

assume A1: v1 = v2 ; :: thesis: G2 .reachableFrom v2 c= G1 .reachableFrom v1

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in G2 .reachableFrom v2 or v in G1 .reachableFrom v1 )

assume v in G2 .reachableFrom v2 ; :: thesis: v in G1 .reachableFrom v1

then consider W being Walk of G2 such that

A2: W is_Walk_from v2,v by Def5;

reconsider W2 = W as Walk of G1 by GLIB_001:167;

W2 is_Walk_from v1,v by A1, A2, GLIB_001:19;

hence v in G1 .reachableFrom v1 by Def5; :: thesis: verum