let G be _Graph; :: thesis: for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)
let C be Component of G; :: thesis: the_Edges_of C = G .edgesBetween (the_Vertices_of C)
reconsider VC = the_Vertices_of C as Subset of (the_Vertices_of G) ;
set EB = G .edgesBetween VC;
C .edgesBetween (the_Vertices_of C) c= G .edgesBetween VC by GLIB_000:79;
then A1: the_Edges_of C c= G .edgesBetween VC by GLIB_000:37;

now

let e be set ; :: thesis: ( ( e in the_Edges_of C implies e in G .edgesBetween VC ) & ( e in G .edgesBetween VC implies e in the_Edges_of C ) )
thus ( e in the_Edges_of C implies e in G .edgesBetween VC ) by A1; :: thesis: ( e in G .edgesBetween VC implies e in the_Edges_of C )
assume A2: e in G .edgesBetween VC ; :: thesis: e in the_Edges_of C

now

consider GX being inducedSubgraph of G,VC,G .edgesBetween VC;
assume A3: not e in the_Edges_of C ; :: thesis: contradiction
A4: the_Edges_of GX = G .edgesBetween VC by GLIB_000:def 39;
the_Vertices_of GX = VC by GLIB_000:def 39;
then A5: C is spanning Subgraph of GX by A1, A4, GLIB_000:47, GLIB_000:def 35;
then GX is connected by Lm10;
then not C c< GX by Def7;
then ( GX == C or not C c= GX ) by GLIB_000:def 38;
hence contradiction by A2, A3, A4, A5, GLIB_000:def 36, GLIB_000:def 37; :: thesis: verum

end;

hence e in the_Edges_of C ; :: thesis: verum

end;

hence the_Edges_of C = G .edgesBetween (the_Vertices_of C) by TARSKI:2; :: thesis: verum