let G be _Graph; :: thesis: ( G is loopfull iff ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive ) )
hereby :: thesis: ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive implies G is loopfull )
assume G is loopfull ; :: thesis: ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive )
then id (the_Vertices_of G) c= VertexAdjSymRel G by Lm4;
hence ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive ) by ROUGHS_1:3; :: thesis: verum
end;
assume ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive ) ; :: thesis: G is loopfull
then id (the_Vertices_of G) c= VertexAdjSymRel G by ROUGHS_1:3;
hence G is loopfull by Lm4; :: thesis: verum