set G = the _finite non _trivial _Graph;
take the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) ; :: thesis: ( not the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) is _trivial & the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) is _finite & the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) is edgeless )
thus ( not the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) is _trivial & the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) is _finite & the removeEdges of the _finite non _trivial _Graph,(the_Edges_of the _finite non _trivial _Graph) is edgeless ) ; :: thesis: verum