let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G1 .componentSet() = G2 .componentSet() )
assume A1: G1 == G2 ; :: thesis:
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:
then consider v1 being Vertex of G1 such that
A2: x = G1 .reachableFrom v1 by Def8;
reconsider v2 = v1 as Vertex of G2 by ;
x = G2 .reachableFrom v2 by A1, A2, Lm9;
hence x in G2 .componentSet() by Def8; :: thesis: verum
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 ;
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