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 .reachableDFrom v2 c= G1 .reachableDFrom 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 .reachableDFrom v2 c= G1 .reachableDFrom v1
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
G2 .reachableDFrom v2 c= G1 .reachableDFrom v1
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies G2 .reachableDFrom v2 c= G1 .reachableDFrom v1 )
assume A1: v1 = v2 ; :: thesis: G2 .reachableDFrom v2 c= G1 .reachableDFrom v1

now

let v be set ; :: thesis: ( v in G2 .reachableDFrom v2 implies v in G1 .reachableDFrom v1 )
assume v in G2 .reachableDFrom v2 ; :: thesis: v in G1 .reachableDFrom v1
then consider W being DWalk of G2 such that
A2: W is_Walk_from v2,v by Def6;
reconsider W = W as DWalk of G1 by GLIB_001:176;
W is_Walk_from v1,v by A1, A2, GLIB_001:20;
hence v in G1 .reachableDFrom v1 by Def6; :: thesis: verum

end;

hence G2 .reachableDFrom v2 c= G1 .reachableDFrom v1 by TARSKI:def 3; :: thesis: verum