let G be _trivial _Graph; :: thesis: ex v being Vertex of G st the_Vertices_of G = {v}
card (the_Vertices_of G) = 1 by Def19;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
reconsider v = v as Vertex of G by A1, TARSKI:def 1;
take v ; :: thesis: the_Vertices_of G = {v}
thus the_Vertices_of G = {v} by A1; :: thesis: verum