set G = the finite trivial _Graph;
take the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) ; :: thesis: ( the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) is trivial & the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) is finite & the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) is edgeless )
thus ( the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) is trivial & the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) is finite & the removeEdges of the finite trivial _Graph,(the_Edges_of the finite trivial _Graph) is edgeless ) ; :: thesis: verum