take the removeEdges of G,(the_Edges_of G) ; :: thesis: ( the removeEdges of G,(the_Edges_of G) is edgeless & the removeEdges of G,(the_Edges_of G) is spanning )
thus ( the removeEdges of G,(the_Edges_of G) is edgeless & the removeEdges of G,(the_Edges_of G) is spanning ) ; :: thesis: verum