let G be _Graph; 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); for H being inducedSubgraph of G,V holds VertexDomRel H = (VertexDomRel G) /\ [:V,V:]
let H be inducedSubgraph of G,V; 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 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 ;
( ( [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 ( [v,w] in (VertexDomRel G) /\ [:V,V:] implies [v,w] in VertexDomRel H )
assume A2:
[v,w] in VertexDomRel H
;
[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;
verum
end; assume
[v,w] in (VertexDomRel G) /\ [:V,V:]
;
[v,w] in VertexDomRel Hthen 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;
verum end;
hence
VertexDomRel H = (VertexDomRel G) /\ [:V,V:]
by RELAT_1:def 2; verum