let G be _Graph; :: thesis: ( G is edgeless iff VertexDomRel G is empty )
thus ( G is edgeless implies VertexDomRel G is empty ) ; :: thesis: ( VertexDomRel G is empty implies G is edgeless )
thus ( VertexDomRel G is empty implies G is edgeless ) :: thesis: verum

proof

assume A1: VertexDomRel G is empty ; :: thesis: G is edgeless
thus G is edgeless :: thesis: verum

proof

assume not G is edgeless ; :: thesis: contradiction
then consider e being object such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G by A2, GLIB_000:def 14;
hence contradiction by A1, Th1; :: thesis: verum

end;

end;