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