let G be _Graph; :: thesis: ( G is loopless iff VertexDomRel G is irreflexive )

hereby :: thesis: ( VertexDomRel G is irreflexive implies G is loopless )

assume G is loopless ; :: thesis: VertexDomRel G is irreflexive
then VertexDomRel G misses id (the_Vertices_of G) by Lm1;
hence VertexDomRel G is irreflexive by GLIBPRE0:11; :: thesis: verum

end;

assume VertexDomRel G is irreflexive ; :: thesis: G is loopless
then VertexDomRel G misses id (the_Vertices_of G) by GLIBPRE0:11;
hence G is loopless by Lm1; :: thesis: verum