let G2 be _Graph; :: thesis: 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 )
let V be set ; :: thesis: 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 )
let G1 be addVertices of G2,V; :: thesis: ( V \ (the_Vertices_of G2) <> {} implies ( not G1 is _trivial & not G1 is connected & not G1 is Tree-like & not G1 is complete ) )
assume V \ (the_Vertices_of G2) <> {} ; :: thesis: ( not G1 is _trivial & not G1 is connected & not G1 is Tree-like & not G1 is complete )
then consider v1 being object such that
A2: v1 in V \ (the_Vertices_of G2) by XBOOLE_0:def 1;
A3: ( v1 in V & not v1 in the_Vertices_of G2 ) by A2, XBOOLE_0:def 5;
then v1 in (the_Vertices_of G2) \/ V by XBOOLE_0:def 3;
then reconsider v1 = v1 as Vertex of G1 by Def10;
set v2 = the Vertex of G2;
v1 <> the Vertex of G2 by A3;
then A5: card {v1, the Vertex of G2} = 2 by CARD_2:57;
the Vertex of G2 in (the_Vertices_of G2) \/ V by XBOOLE_0:def 3;
then the Vertex of G2 in the_Vertices_of G1 by Def10;
then A6: 2 c= card (the_Vertices_of G1) by A5, CARD_1:11, ZFMISC_1:32;
card (the_Vertices_of G1) <> 1

proof

assume card (the_Vertices_of G1) = 1 ; :: thesis: contradiction
then 1 in 1 by A6, CARD_2:69;
hence contradiction ; :: thesis: verum

end;

hence A7: not G1 is _trivial by GLIB_000:def 19; :: thesis: ( not G1 is connected & not G1 is Tree-like & not G1 is complete )
v1 is isolated by A2, Th92;
hence ( not G1 is connected & not G1 is Tree-like & not G1 is complete ) by A7, GLIB_002:2; :: thesis: verum