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:76;
then A1: the_Edges_of C c= G .edgesBetween VC by GLIB_000:34;

now :: thesis: for e being object holds
( ( e in the_Edges_of C implies e in G .edgesBetween VC ) & ( e in G .edgesBetween VC implies e in the_Edges_of C ) )

let e be object ; :: 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 :: thesis: e in the_Edges_of C

set GX = the inducedSubgraph of G,VC,G .edgesBetween VC;
assume A3: not e in the_Edges_of C ; :: thesis: contradiction
A4: the_Edges_of the inducedSubgraph of G,VC,G .edgesBetween VC = G .edgesBetween VC by GLIB_000:def 37;
the_Vertices_of the inducedSubgraph of G,VC,G .edgesBetween VC = VC by GLIB_000:def 37;
then A5: C is spanning Subgraph of the inducedSubgraph of G,VC,G .edgesBetween VC by A1, A4, GLIB_000:44, GLIB_000:def 33;
then the inducedSubgraph of G,VC,G .edgesBetween VC is connected by Lm10;
then not C c< the inducedSubgraph of G,VC,G .edgesBetween VC by Def7;
then ( the inducedSubgraph of G,VC,G .edgesBetween VC == C or not C c= the inducedSubgraph of G,VC,G .edgesBetween VC ) by GLIB_000:def 36;
hence contradiction by A2, A3, A4, A5, GLIB_000:def 34, GLIB_000:def 35; :: 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