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

now :: thesis: for x being object holds

( ( x in union (G .componentSet()) implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in union (G .componentSet()) ) )

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

let x be object ; :: 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 x9 = x as Vertex of G ;

set Y = G .reachableFrom x9;

( x in G .reachableFrom x9 & G .reachableFrom x9 in G .componentSet() ) by Def8, Lm1;

hence x in union (G .componentSet()) by TARSKI:def 4; :: thesis: verum

end;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 x9 = x as Vertex of G ;

set Y = G .reachableFrom x9;

( x in G .reachableFrom x9 & G .reachableFrom x9 in G .componentSet() ) by Def8, Lm1;

hence x in union (G .componentSet()) by TARSKI:def 4; :: thesis: verum