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

now :: thesis: for G4 being connected Subgraph of G2 holds not G3 c< G4

given G4 being connected Subgraph of G2 such that A2: G3 c< G4 ; :: thesis: contradiction
G4 is Subgraph of G1 by A1, GLIB_000:91;
hence contradiction by A2, GLIB_002:def 7; :: thesis: verum

end;

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