let G be _Graph; :: thesis: union (G .componentSet() ) = the_Vertices_of G

now

let x be set ; :: thesis: ( ( x in union (G .componentSet() ) implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in union (G .componentSet() ) ) )
thus ( x in union (G .componentSet() ) implies x in the_Vertices_of G ) ; :: thesis: ( x in the_Vertices_of G implies x in union (G .componentSet() ) )
assume x in the_Vertices_of G ; :: thesis: x in union (G .componentSet() )
then reconsider x' = x as Vertex of ;
set Y = G .reachableFrom x';
( x in G .reachableFrom x' & G .reachableFrom x' in G .componentSet() ) by Def8, Lm1;
hence x in union (G .componentSet() ) by TARSKI:def 4; :: thesis: verum

end;

hence union (G .componentSet() ) = the_Vertices_of G by TARSKI:2; :: thesis: verum