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

assume A1: G1 == G2 ; :: thesis: 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() ) )

hence
G1 .componentSet() = G2 .componentSet()
by TARSKI:2; :: thesis: verum( ( 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() ) )

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

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

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