let G be _Graph; :: thesis: for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G)
let x be set ; :: thesis: ( x in G .componentSet() implies x is non empty Subset of (the_Vertices_of G) )
assume x in G .componentSet() ; :: thesis: x is non empty Subset of (the_Vertices_of G)
then ex v being Vertex of G st x = G .reachableFrom v by Def8;
hence x is non empty Subset of (the_Vertices_of G) ; :: thesis: verum