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;

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 ) )

hence
the_Edges_of C = G .edgesBetween (the_Vertices_of C)
by TARSKI:2; :: thesis: verum( ( 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

end;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

hence
e in the_Edges_of C
; :: thesis: verumset 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;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