theorem :: GLIB_000:27

for G being finite _Graph holds
( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} )