let G be _Graph; :: thesis: for H being removeEdges of G,(the_Edges_of G) holds H == createGraph ([#] (the_Vertices_of G))
let H be removeEdges of G,(the_Edges_of G); :: thesis: H == createGraph ([#] (the_Vertices_of G))
( (the_Edges_of G) \ (the_Edges_of G) = {} & [#] (the_Vertices_of G) = the_Vertices_of G ) by XBOOLE_1:37;
hence H == createGraph ([#] (the_Vertices_of G)) by Th5; :: thesis: verum