let G be _Graph; :: thesis: ( G is edgeless iff G == createGraph ([#] (the_Vertices_of G)) )
set H = the removeEdges of G,(the_Edges_of G);

hereby :: thesis: ( G == createGraph ([#] (the_Vertices_of G)) implies G is edgeless )

assume G is edgeless ; :: thesis: G == createGraph ([#] (the_Vertices_of G))
then A1: the_Edges_of G = the_Edges_of the removeEdges of G,(the_Edges_of G) ;
A2: the_Vertices_of G = the_Vertices_of the removeEdges of G,(the_Edges_of G) by GLIB_000:def 33;
G is Subgraph of G by GLIB_000:40;
then A3: G == the removeEdges of G,(the_Edges_of G) by A1, A2, GLIB_000:86;
the removeEdges of G,(the_Edges_of G) == createGraph ([#] (the_Vertices_of G)) by Th6;
hence G == createGraph ([#] (the_Vertices_of G)) by A3, GLIB_000:85; :: thesis: verum

end;

assume G == createGraph ([#] (the_Vertices_of G)) ; :: thesis: G is edgeless
hence G is edgeless by GLIB_008:52; :: thesis: verum