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;

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

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

now :: thesis: contradiction

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

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

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

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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