let G be _Graph; :: thesis: for V being Subset of (the_Vertices_of G)
for H being addLoops of G,V holds VertexDomRel H = (VertexDomRel G) \/ (id V)
let V be Subset of (the_Vertices_of G); :: thesis: for H being addLoops of G,V holds VertexDomRel H = (VertexDomRel G) \/ (id V)
let H be addLoops of G,V; :: thesis: VertexDomRel H = (VertexDomRel G) \/ (id V)
consider E being set , f being one-to-one Function such that
A1: ( E misses the_Edges_of G & the_Edges_of H = (the_Edges_of G) \/ E ) and
A2: ( dom f = E & rng f = V ) and
A3: the_Source_of H = (the_Source_of G) +* f and
A4: the_Target_of H = (the_Target_of G) +* f by GLIB_012:def 5;

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

let v, w be object ; :: thesis: ( ( [v,w] in VertexDomRel H implies [v,w] in (VertexDomRel G) \/ (id V) ) & ( [v,w] in (VertexDomRel G) \/ (id V) implies [b₁,b₂] in VertexDomRel H ) )

hereby :: thesis: ( [v,w] in (VertexDomRel G) \/ (id V) implies [b₁,b₂] in VertexDomRel H )

assume [v,w] in VertexDomRel H ; :: thesis: [v,w] in (VertexDomRel G) \/ (id V)
then consider e being object such that
A5: e DJoins v,w,H by Th1;

per cases ( e DJoins v,w,G or not e in the_Edges_of G ) by A5, GLIB_006:71;

suppose e DJoins v,w,G ; :: thesis: [v,w] in (VertexDomRel G) \/ (id V)

then [v,w] in VertexDomRel G by Th1;
hence [v,w] in (VertexDomRel G) \/ (id V) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A6: not e in the_Edges_of G ; :: thesis: [v,w] in (VertexDomRel G) \/ (id V)

e in the_Edges_of H by A5, GLIB_000:def 14;
then A7: e in E by A1, A6, XBOOLE_0:def 3;
A8: v = (the_Source_of H) . e by A5, GLIB_000:def 14
.= f . e by A2, A3, A7, FUNCT_4:13 ;
w = (the_Target_of H) . e by A5, GLIB_000:def 14
.= f . e by A2, A4, A7, FUNCT_4:13 ;
then A9: v = w by A8;
v in V by A2, A7, A8, FUNCT_1:3;
then [v,w] in id V by A9, RELAT_1:def 10;
hence [v,w] in (VertexDomRel G) \/ (id V) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume [v,w] in (VertexDomRel G) \/ (id V) ; :: thesis: [b₁,b₂] in VertexDomRel H

per cases then ( [v,w] in VertexDomRel G or [v,w] in id V ) by XBOOLE_0:def 3;

suppose A10: [v,w] in VertexDomRel G ; :: thesis: [b₁,b₂] in VertexDomRel H

G is Subgraph of H by GLIB_006:57;
hence [v,w] in VertexDomRel H by A10, Th15, TARSKI:def 3; :: thesis: verum

end;

suppose [v,w] in id V ; :: thesis: [b₁,b₂] in VertexDomRel H

then A11: ( v = w & v in V ) by RELAT_1:def 10;
then reconsider v0 = v as Vertex of H by GLIB_012:def 5;
v0,v0 are_adjacent by A11, GLIB_012:18;
then consider e being object such that
A12: e Joins v,v,H by CHORD:def 3;
e DJoins v,v,H by A12, GLIB_000:16;
hence [v,w] in VertexDomRel H by A11, Th1; :: thesis: verum

end;

end;

end;

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