let G be _Graph; :: thesis: for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )
let C1, C2 be Component of G; :: thesis: ( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )

hereby :: thesis: ( C1 == C2 implies the_Vertices_of C1 = the_Vertices_of C2 )

assume A1: the_Vertices_of C1 = the_Vertices_of C2 ; :: thesis: C1 == C2
then the_Edges_of C1 = G .edgesBetween (the_Vertices_of C2) by Lm14
.= the_Edges_of C2 by Lm14 ;
hence C1 == C2 by A1, GLIB_000:86; :: thesis: verum

end;

assume C1 == C2 ; :: thesis: the_Vertices_of C1 = the_Vertices_of C2
hence the_Vertices_of C1 = the_Vertices_of C2 by GLIB_000:def 34; :: thesis: verum