let G be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds VertexDomRel H = (VertexDomRel G) /\ [:V,V:]
let V be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,V holds VertexDomRel H = (VertexDomRel G) /\ [:V,V:]
let H be inducedSubgraph of G,V; :: thesis: VertexDomRel H = (VertexDomRel G) /\ [:V,V:]
A1: ( the_Vertices_of H = V & the_Edges_of H = G .edgesBetween V ) by GLIB_000:def 37;

now :: thesis: for v, w being object holds
( ( [v,w] in VertexDomRel H implies [v,w] in (VertexDomRel G) /\ [:V,V:] ) & ( [v,w] in (VertexDomRel G) /\ [:V,V:] implies [v,w] in VertexDomRel H ) )

let v, w be object ; :: thesis: ( ( [v,w] in VertexDomRel H implies [v,w] in (VertexDomRel G) /\ [:V,V:] ) & ( [v,w] in (VertexDomRel G) /\ [:V,V:] implies [v,w] in VertexDomRel H ) )

hereby :: thesis: ( [v,w] in (VertexDomRel G) /\ [:V,V:] implies [v,w] in VertexDomRel H )

assume A2: [v,w] in VertexDomRel H ; :: thesis: [v,w] in (VertexDomRel G) /\ [:V,V:]
then consider e being object such that
A3: e DJoins v,w,H by Th1;
e Joins v,w,H by A3, GLIB_000:16;
then ( v in V & w in V ) by A1, GLIB_000:13;
then A4: [v,w] in [:V,V:] by ZFMISC_1:87;
[v,w] in VertexDomRel G by A2, Th15, TARSKI:def 3;
hence [v,w] in (VertexDomRel G) /\ [:V,V:] by A4, XBOOLE_0:def 4; :: thesis: verum

end;

assume [v,w] in (VertexDomRel G) /\ [:V,V:] ; :: thesis: [v,w] in VertexDomRel H
then A5: ( [v,w] in VertexDomRel G & [v,w] in [:V,V:] ) by XBOOLE_0:def 4;
then consider e being object such that
A6: e DJoins v,w,G by Th1;
A7: ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by A6, GLIB_000:def 14;
( v in V & w in V ) by A5, ZFMISC_1:87;
then A8: e in the_Edges_of H by A1, A7, GLIB_000:31;
( e is set & v is set & w is set ) by TARSKI:1;
then e DJoins v,w,H by A6, A8, GLIB_000:73;
hence [v,w] in VertexDomRel H by Th1; :: thesis: verum

end;

hence VertexDomRel H = (VertexDomRel G) /\ [:V,V:] by RELAT_1:def 2; :: thesis: verum