let G be _Graph; :: thesis:
thus ( G is Component of G implies G is connected ) ; :: thesis:
A1: G is Subgraph of G by GLIB_000:40;

A2: now :: thesis:

given G2 being connected Subgraph of G such that A3: G c< G2 ; :: thesis:

per cases by A1, A3, GLIB_000:98;

suppose the_Vertices_of G c< the_Vertices_of G2 ; :: thesis:

hence contradiction by XBOOLE_0:def 8; :: thesis:

end;

suppose the_Edges_of G c< the_Edges_of G2 ; :: thesis:

hence contradiction by XBOOLE_0:def 8; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

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