let G2 be removeEdges of G,(the_Edges_of G); :: thesis: G2 is edgeless
the_Edges_of G2 = (the_Edges_of G) \ (the_Edges_of G) by GLIB_000:53
.= {} by XBOOLE_1:37 ;
hence G2 is edgeless ; :: thesis: verum