let G be _Graph; :: thesis: for H being Subgraph of G holds VertexDomRel H c= VertexDomRel G
let H be Subgraph of G; :: thesis: VertexDomRel H c= VertexDomRel G
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
A1: e DJoins v,w,H by Th1;
( e is set & v is set & w is set ) by TARSKI:1;
then e DJoins v,w,G by A1, GLIB_000:72;
hence [v,w] in VertexDomRel G by Th1; :: thesis: verum
end;
hence VertexDomRel H c= VertexDomRel G by RELAT_1:def 3; :: thesis: verum