let G be _Graph; :: thesis: ( G is loopfull iff ( VertexDomRel G is total & VertexDomRel G is reflexive ) )

hereby :: thesis: ( VertexDomRel G is total & VertexDomRel G is reflexive implies G is loopfull )

assume G is loopfull ; :: thesis: ( VertexDomRel G is total & VertexDomRel G is reflexive )
then id (the_Vertices_of G) c= VertexDomRel G by Lm2;
hence ( VertexDomRel G is total & VertexDomRel G is reflexive ) by ROUGHS_1:3; :: thesis: verum

end;

assume ( VertexDomRel G is total & VertexDomRel G is reflexive ) ; :: thesis: G is loopfull
then id (the_Vertices_of G) c= VertexDomRel G by ROUGHS_1:3;
hence G is loopfull by Lm2; :: thesis: verum