let G be _Graph; :: thesis: ( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} )

hereby :: thesis: ( ex v being Vertex of G st the_Vertices_of G = {v} implies G .order() = 1 )

assume G .order() = 1 ; :: thesis: ex v being Vertex of G st the_Vertices_of G = {v}
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 = v; :: thesis: the_Vertices_of G = {v}
thus the_Vertices_of G = {v} by A1; :: thesis: verum

end;

given v being Vertex of G such that A2: the_Vertices_of G = {v} ; :: thesis: G .order() = 1
thus G .order() = 1 by A2, CARD_1:30; :: thesis: verum