let G1, G2 be _Graph; :: thesis: for G3 being Component of G1 st G2 == G3 holds
G2 is Component of G1
let G3 be Component of G1; :: thesis: ( G2 == G3 implies G2 is Component of G1 )
assume A1: G2 == G3 ; :: thesis: G2 is Component of G1

now :: thesis: ( G2 is connected & ( for G9 being connected Subgraph of G1 holds not G2 c< G9 ) )

thus G2 is connected by A1, GLIB_002:8; :: thesis: for G9 being connected Subgraph of G1 holds not G2 c< G9
given G9 being connected Subgraph of G1 such that A2: G2 c< G9 ; :: thesis: contradiction
A3: ( G2 c= G9 & G2 != G9 ) by A2, GLIB_000:def 36;
then G2 is Subgraph of G9 by GLIB_000:def 35;
then A4: G3 is Subgraph of G9 by A1, GLIB_000:92;
G3 != G9 by A1, A3, GLIB_000:85;
then G3 c< G9 by A4, GLIB_000:def 35, GLIB_000:def 36;
hence contradiction by GLIB_002:def 7; :: thesis: verum

end;

hence G2 is Component of G1 by A1, GLIB_000:92, GLIB_002:def 7; :: thesis: verum