let G be _Graph; :: thesis: ( G is loopfull iff id (the_Vertices_of G) c= VertexDomRel G )

hereby :: thesis: ( id (the_Vertices_of G) c= VertexDomRel G implies G is loopfull )

assume A1: G is loopfull ; :: thesis: id (the_Vertices_of G) c= VertexDomRel G

now :: thesis: for x, y being object st [x,y] in id (the_Vertices_of G) holds
[x,y] in VertexDomRel G

let x, y be object ; :: thesis: ( [x,y] in id (the_Vertices_of G) implies [x,y] in VertexDomRel G )
assume [x,y] in id (the_Vertices_of G) ; :: thesis: [x,y] in VertexDomRel G
then A2: ( x in the_Vertices_of G & x = y ) by RELAT_1:def 10;
then ex e being object st e DJoins x,x,G by A1, GLIB_012:1;
hence [x,y] in VertexDomRel G by A2, Th1; :: thesis: verum

end;

hence id (the_Vertices_of G) c= VertexDomRel G by RELAT_1:def 3; :: thesis: verum

end;

assume A3: id (the_Vertices_of G) c= VertexDomRel G ; :: thesis: G is loopfull

now :: thesis: for v being Vertex of G ex e being object st e DJoins v,v,G

let v be Vertex of G; :: thesis: ex e being object st e DJoins v,v,G
[v,v] in id (the_Vertices_of G) by RELAT_1:def 10;
hence ex e being object st e DJoins v,v,G by A3, Th1; :: thesis: verum

end;

hence G is loopfull by GLIB_012:1; :: thesis: verum