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 )

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

( 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
C1 == C2
; :: thesis: the_Vertices_of C1 = the_Vertices_of C2assume 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;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

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