set G0 = the _Graph;
set G = the addVertex of the _Graph,(the_Vertices_of the _Graph);
take the addVertex of the _Graph,(the_Vertices_of the _Graph) ; :: thesis: ( not the addVertex of the _Graph,(the_Vertices_of the _Graph) is _trivial & not the addVertex of the _Graph,(the_Vertices_of the _Graph) is connected & not the addVertex of the _Graph,(the_Vertices_of the _Graph) is complete )
thus ( not the addVertex of the _Graph,(the_Vertices_of the _Graph) is _trivial & not the addVertex of the _Graph,(the_Vertices_of the _Graph) is connected & not the addVertex of the _Graph,(the_Vertices_of the _Graph) is complete ) ; :: thesis: verum