let G be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V
for E being RepDEdgeSelection of G holds E /\ (G .edgesBetween V) is RepDEdgeSelection of H
let V be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,V
for E being RepDEdgeSelection of G holds E /\ (G .edgesBetween V) is RepDEdgeSelection of H
let H be inducedSubgraph of G,V; :: thesis: for E being RepDEdgeSelection of G holds E /\ (G .edgesBetween V) is RepDEdgeSelection of H
let E be RepDEdgeSelection of G; :: thesis: E /\ (G .edgesBetween V) is RepDEdgeSelection of H
G .edgesBetween V = the_Edges_of H by GLIB_000:def 37;
then reconsider E9 = E /\ (G .edgesBetween V) as Subset of (the_Edges_of H) by XBOOLE_1:17;

now :: thesis: for v, w, e0 being object st e0 DJoins v,w,H holds
ex e being object st
( e DJoins v,w,H & e in E9 & ( for e9 being object st e9 DJoins v,w,H & e9 in E9 holds
e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 DJoins v,w,H implies ex e being object st
( e DJoins v,w,H & e in E9 & ( for e9 being object st e9 DJoins v,w,H & e9 in E9 holds
e9 = e ) ) )
A1: ( v is set & w is set ) by TARSKI:1;
assume A2: e0 DJoins v,w,H ; :: thesis: ex e being object st
( e DJoins v,w,H & e in E9 & ( for e9 being object st e9 DJoins v,w,H & e9 in E9 holds
e9 = e ) )
then e0 DJoins v,w,G by A1, GLIB_000:72;
then consider e being object such that
A3: ( e DJoins v,w,G & e in E ) and
A4: for e9 being object st e9 DJoins v,w,G & e9 in E holds
e9 = e by GLIB_009:def 6;
take e = e; :: thesis: ( e DJoins v,w,H & e in E9 & ( for e9 being object st e9 DJoins v,w,H & e9 in E9 holds
e9 = e ) )
e0 Joins v,w,H by A2, GLIB_000:16;
then ( v in the_Vertices_of H & w in the_Vertices_of H ) by GLIB_000:13;
then A5: ( v in V & w in V ) by GLIB_000:def 37;
e Joins v,w,G by A3, GLIB_000:16;
then A6: e in G .edgesBetween V by A5, GLIB_000:32;
then e in the_Edges_of H by GLIB_000:def 37;
hence e DJoins v,w,H by A1, A3, GLIB_000:73; :: thesis: ( e in E9 & ( for e9 being object st e9 DJoins v,w,H & e9 in E9 holds
e9 = e ) )
thus e in E9 by A3, A6, XBOOLE_0:def 4; :: thesis: for e9 being object st e9 DJoins v,w,H & e9 in E9 holds
e9 = e
let e9 be object ; :: thesis: ( e9 DJoins v,w,H & e9 in E9 implies e9 = e )
assume ( e9 DJoins v,w,H & e9 in E9 ) ; :: thesis: e9 = e
then ( e9 DJoins v,w,G & e9 in E ) by A1, GLIB_000:72, XBOOLE_0:def 4;
hence e9 = e by A4; :: thesis: verum

end;

hence E /\ (G .edgesBetween V) is RepDEdgeSelection of H by GLIB_009:def 6; :: thesis: verum