let G be _Graph; :: thesis: ( G is edgeless iff VertexAdjSymRel G is empty )
hereby :: thesis: ( VertexAdjSymRel G is empty implies G is edgeless )
assume G is edgeless ; :: thesis: VertexAdjSymRel G is empty
then VertexDomRel G is empty ;
hence VertexAdjSymRel G is empty ; :: thesis: verum
end;
thus ( VertexAdjSymRel G is empty implies G is edgeless ) ; :: thesis: verum