let G be _Graph; for H being removeLoops of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
let H be removeLoops of G; VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
now 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 ;
( ( [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 ( [v,w] in (VertexDomRel G) \ (id (the_Vertices_of G)) implies [v,w] in VertexDomRel H )
assume A1:
[v,w] in VertexDomRel H
;
[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_009:17;
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;
verum
end; assume
[v,w] in (VertexDomRel G) \ (id (the_Vertices_of G))
;
[v,w] in VertexDomRel Hthen 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;
verum end;
hence
VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
by RELAT_1:def 2; verum