let G1 be addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G; :: 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 ) ;
hence not G1 is _trivial by Th147; :: thesis: verum