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