let G1, G2 be _Graph; :: thesis:
assume A1: G1 == G2 ; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in G1 .componentSet() ; :: thesis:
then consider v1 being Vertex of G1 such that
A2: x = G1 .reachableFrom v1 by Def8;
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = G2 .reachableFrom v2 by A1, A2, Lm9;
hence x in G2 .componentSet() by Def8; :: thesis:

end;

assume x in G2 .componentSet() ; :: thesis:
then consider v2 being Vertex of G2 such that
A3: x = G2 .reachableFrom v2 by Def8;
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = G1 .reachableFrom v1 by A1, A3, Lm9;
hence x in G1 .componentSet() by Def8; :: thesis:

end;

hence G1 .componentSet() = G2 .componentSet() by TARSKI:2; :: thesis: