let G1 be addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v; :: thesis: not G1 is _trivial
( not the_Edges_of G in the_Edges_of G & not the_Vertices_of G in the_Vertices_of G ) ;
then consider G3 being addVertex of G,(the_Vertices_of G) such that
A1: G1 is addEdge of G3, the_Vertices_of G, the_Edges_of G,v by Th130;
thus not G1 is _trivial by A1; :: thesis: verum