set G2 = the _trivial _Graph;
set G1 = the addEdge of the _trivial _Graph, the Vertex of the _trivial _Graph, the_Edges_of the _trivial _Graph, the Vertex of the _trivial _Graph;
take the addEdge of the _trivial _Graph, the Vertex of the _trivial _Graph, the_Edges_of the _trivial _Graph, the Vertex of the _trivial _Graph ; :: thesis: ( the addEdge of the _trivial _Graph, the Vertex of the _trivial _Graph, the_Edges_of the _trivial _Graph, the Vertex of the _trivial _Graph is loopfull & the addEdge of the _trivial _Graph, the Vertex of the _trivial _Graph, the_Edges_of the _trivial _Graph, the Vertex of the _trivial _Graph is complete )
thus ( the addEdge of the _trivial _Graph, the Vertex of the _trivial _Graph, the_Edges_of the _trivial _Graph, the Vertex of the _trivial _Graph is loopfull & the addEdge of the _trivial _Graph, the Vertex of the _trivial _Graph, the_Edges_of the _trivial _Graph, the Vertex of the _trivial _Graph is complete ) ; :: thesis: verum