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 )
assume A1: G is connected ; :: thesis: G is Component of G
A2: G is Subgraph of G by GLIB_000:43;

now

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

now

per cases ( the_Vertices_of G c< the_Vertices_of G2 or the_Edges_of G c< the_Edges_of G2 ) by A2, A3, GLIB_000:101;

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;

hence G is Component of G by A1, Def7, GLIB_000:43; :: thesis: verum