let G be _Graph; for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)
let C be Component of G; 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 let e be
set ;
( ( 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;
( e in G .edgesBetween VC implies e in the_Edges_of C )assume A2:
e in G .edgesBetween VC
;
e in the_Edges_of Cnow set GX = the
inducedSubgraph of
G,
VC,
G .edgesBetween VC;
assume A3:
not
e in the_Edges_of C
;
contradictionA4:
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;
verum end; hence
e in the_Edges_of C
;
verum end;
hence
the_Edges_of C = G .edgesBetween (the_Vertices_of C)
by TARSKI:1; verum