set G0 = the loopless _trivial _Graph;
set v = the Vertex of the loopless _trivial _Graph;
set G = the addAdjVertex of the loopless _trivial _Graph, the Vertex of the loopless _trivial _Graph, the_Edges_of the loopless _trivial _Graph, the_Vertices_of the loopless _trivial _Graph;
take the addAdjVertex of the loopless _trivial _Graph, the Vertex of the loopless _trivial _Graph, the_Edges_of the loopless _trivial _Graph, the_Vertices_of the loopless _trivial _Graph ; :: thesis: ( the addAdjVertex of the loopless _trivial _Graph, the Vertex of the loopless _trivial _Graph, the_Edges_of the loopless _trivial _Graph, the_Vertices_of the loopless _trivial _Graph is loopless & not the addAdjVertex of the loopless _trivial _Graph, the Vertex of the loopless _trivial _Graph, the_Edges_of the loopless _trivial _Graph, the_Vertices_of the loopless _trivial _Graph is edgeless )
thus ( the addAdjVertex of the loopless _trivial _Graph, the Vertex of the loopless _trivial _Graph, the_Edges_of the loopless _trivial _Graph, the_Vertices_of the loopless _trivial _Graph is loopless & not the addAdjVertex of the loopless _trivial _Graph, the Vertex of the loopless _trivial _Graph, the_Edges_of the loopless _trivial _Graph, the_Vertices_of the loopless _trivial _Graph is edgeless ) ; :: thesis: verum