theorem Th93: :: GLIB_006:89

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
( not G1 is _trivial & not G1 is connected & not G1 is Tree-like & not G1 is complete )