let G be _Graph; :: thesis: ( G is Component of G iff G is connected )

thus ( G is Component of G implies G is connected ) ; :: thesis: ( G is connected implies G is Component of G )

A1: G is Subgraph of G by GLIB_000:40;

hence G is Component of G by A2, Def7, GLIB_000:40; :: thesis: verum

thus ( G is Component of G implies G is connected ) ; :: thesis: ( G is connected implies G is Component of G )

A1: G is Subgraph of G by GLIB_000:40;

A2: now :: thesis: for G2 being connected Subgraph of G holds not G c< G2

assume
G is connected
; :: thesis: G is Component of Ggiven G2 being connected Subgraph of G such that A3:
G c< G2
; :: thesis: contradiction

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( the_Vertices_of G c< the_Vertices_of G2 or the_Edges_of G c< the_Edges_of G2 )
by A1, A3, GLIB_000:98;

end;

hence G is Component of G by A2, Def7, GLIB_000:40; :: thesis: verum