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