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

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