let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G1 .componentSet() = G2 .componentSet() )
assume A1: G1 == G2 ; :: thesis: G1 .componentSet() = G2 .componentSet()

now :: thesis: for x being object holds
( ( x in G1 .componentSet() implies x in G2 .componentSet() ) & ( x in G2 .componentSet() implies x in G1 .componentSet() ) )

let x be object ; :: thesis: ( ( x in G1 .componentSet() implies x in G2 .componentSet() ) & ( x in G2 .componentSet() implies x in G1 .componentSet() ) )

hereby :: thesis: ( x in G2 .componentSet() implies x in G1 .componentSet() )

assume x in G1 .componentSet() ; :: thesis: x in G2 .componentSet()
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: verum

end;

assume x in G2 .componentSet() ; :: thesis: x in G1 .componentSet()
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: verum

end;

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