let G1 be addVertex of G,(the_Vertices_of G); :: thesis: ( not G1 is _trivial & not G1 is connected & not G1 is complete )
{(the_Vertices_of G)} \ (the_Vertices_of G) <> {} by Lm1;
hence ( not G1 is _trivial & not G1 is connected & not G1 is complete ) by Th93; :: thesis: verum