let G be _Graph; :: thesis: ( G is loopless iff VertexDomRel G misses id (the_Vertices_of G) )
set V = the_Vertices_of G;

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

assume A1: G is loopless ; :: thesis: VertexDomRel G misses id (the_Vertices_of G)
(VertexDomRel G) /\ (id (the_Vertices_of G)) = {}

proof

assume (VertexDomRel G) /\ (id (the_Vertices_of G)) <> {} ; :: thesis: contradiction
then consider z being object such that
A2: z in (VertexDomRel G) /\ (id (the_Vertices_of G)) by XBOOLE_0:def 1;
consider x, y being object such that
A3: z = [x,y] by A2, RELAT_1:def 1;
A4: ( [x,y] in VertexDomRel G & [x,y] in id (the_Vertices_of G) ) by A2, A3, XBOOLE_0:def 4;
then x = y by RELAT_1:def 10;
then ex e being object st e DJoins x,x,G by A4, Th1;
hence contradiction by A1, GLIB_000:136; :: thesis: verum

end;

hence VertexDomRel G misses id (the_Vertices_of G) by XBOOLE_0:def 7; :: thesis: verum

end;

assume VertexDomRel G misses id (the_Vertices_of G) ; :: thesis: G is loopless
then A5: (VertexDomRel G) /\ (id (the_Vertices_of G)) = {} by XBOOLE_0:def 7;
assume not G is loopless ; :: thesis: contradiction
then consider v, e being object such that
A6: e DJoins v,v,G by GLIB_000:136;
A7: [v,v] in VertexDomRel G by A6, Th1;
e Joins v,v,G by A6, GLIB_000:16;
then v in the_Vertices_of G by GLIB_000:13;
then [v,v] in id (the_Vertices_of G) by RELAT_1:def 10;
hence contradiction by A5, A7, XBOOLE_0:def 4; :: thesis: verum