let G be _Graph; :: thesis: for V being set
for H being addVertices of G,V holds VertexDomRel H = VertexDomRel G
let V be set ; :: thesis: for H being addVertices of G,V holds VertexDomRel H = VertexDomRel G
let H be addVertices of G,V; :: thesis: VertexDomRel H = VertexDomRel G
G is Subgraph of H by GLIB_006:57;
then A1: VertexDomRel G c= VertexDomRel H by Th15;
now :: thesis: for v, w being object st [v,w] in VertexDomRel H holds
[v,w] in VertexDomRel G
let v, w be object ; :: thesis: ( [v,w] in VertexDomRel H implies [v,w] in VertexDomRel G )
assume [v,w] in VertexDomRel H ; :: thesis: [v,w] in VertexDomRel G
then consider e being object such that
A2: e DJoins v,w,H by Th1;
e DJoins v,w,G by A2, GLIB_006:85;
hence [v,w] in VertexDomRel G by Th1; :: thesis: verum
end;
then VertexDomRel H c= VertexDomRel G by RELAT_1:def 3;
hence VertexDomRel H = VertexDomRel G by A1, XBOOLE_0:def 10; :: thesis: verum