let G be _Graph; :: thesis: ( G is loopless iff VertexAdjSymRel G is irreflexive )
thus ( G is loopless implies VertexAdjSymRel G is irreflexive ) ; :: thesis: ( VertexAdjSymRel G is irreflexive implies G is loopless )
assume VertexAdjSymRel G is irreflexive ; :: thesis: G is loopless
then VertexAdjSymRel G misses id (the_Vertices_of G) by GLIBPRE0:11;
hence G is loopless by Lm3; :: thesis: verum