let G be _Graph; :: thesis: ( G is loopless iff VertexAdjSymRel G misses id (the_Vertices_of G) )

hereby :: thesis: ( VertexAdjSymRel G misses id (the_Vertices_of G) implies G is loopless )

set H = the reverseEdgeDirections of G;
A1: VertexDomRel the reverseEdgeDirections of G = (VertexDomRel G) ~ by Th20;
assume A2: G is loopless ; :: thesis: VertexAdjSymRel G misses id (the_Vertices_of G)
then A3: VertexDomRel G misses id (the_Vertices_of G) by Lm1;
VertexDomRel the reverseEdgeDirections of G misses id (the_Vertices_of the reverseEdgeDirections of G) by A2, Lm1;
then (VertexDomRel G) ~ misses id (the_Vertices_of G) by A1, GLIB_007:4;
hence VertexAdjSymRel G misses id (the_Vertices_of G) by A3, XBOOLE_1:70; :: thesis: verum

end;

assume VertexAdjSymRel G misses id (the_Vertices_of G) ; :: thesis: G is loopless
then VertexDomRel G misses id (the_Vertices_of G) by XBOOLE_1:70;
hence G is loopless by Lm1; :: thesis: verum