let G be _Graph; :: thesis: for H being removeLoops of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
let H be removeLoops of G; :: thesis: VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))

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

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

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

assume A1: [v,w] in VertexDomRel H ; :: thesis: [v,w] in (VertexDomRel G) \ (id (the_Vertices_of G))
then consider e being object such that
A2: e DJoins v,w,H by Th1;
v <> w by A2, GLIB_000:136;
then A3: not [v,w] in id (the_Vertices_of G) by RELAT_1:def 10;
[v,w] in VertexDomRel G by A1, Th15, TARSKI:def 3;
hence [v,w] in (VertexDomRel G) \ (id (the_Vertices_of G)) by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume [v,w] in (VertexDomRel G) \ (id (the_Vertices_of G)) ; :: thesis: [v,w] in VertexDomRel H
then A4: ( [v,w] in VertexDomRel G & not [v,w] in id (the_Vertices_of G) ) by XBOOLE_0:def 5;
then consider e being object such that
A5: e DJoins v,w,G by Th1;
A6: e Joins v,w,G by A5, GLIB_000:16;
then v in the_Vertices_of G by GLIB_000:13;
then v <> w by A4, RELAT_1:def 10;
then A7: not e in G .loops() by A6, GLIB_009:46;
e in the_Edges_of G by A5, GLIB_000:def 14;
then e in (the_Edges_of G) \ (G .loops()) by A7, XBOOLE_0:def 5;
then A8: e in the_Edges_of H by GLIB_000:53;
( v is set & w is set & e is set ) by TARSKI:1;
then e DJoins v,w,H by A5, A8, GLIB_000:73;
hence [v,w] in VertexDomRel H by Th1; :: thesis: verum

end;

hence VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G)) by RELAT_1:def 2; :: thesis: verum