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

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

assume G is loopfull ; :: thesis: id (the_Vertices_of G) c= VertexAdjSymRel G
then A1: id (the_Vertices_of G) c= VertexDomRel G by Lm2;
VertexDomRel G c= VertexAdjSymRel G by Th34;
hence id (the_Vertices_of G) c= VertexAdjSymRel G by A1, XBOOLE_1:1; :: thesis: verum

end;

assume A2: id (the_Vertices_of G) c= VertexAdjSymRel G ; :: thesis: G is loopfull

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

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

end;

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