let G1, G2 be _Graph; :: thesis: ( G1 == G2 iff G1 .allComponents() = G2 .allComponents() )

hereby :: thesis: ( G1 .allComponents() = G2 .allComponents() implies G1 == G2 )

assume A1: G1 == G2 ; :: thesis: G1 .allComponents() = G2 .allComponents()

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

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

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

assume x in G1 .allComponents() ; :: thesis: x in G2 .allComponents()
then reconsider C = x as plain Component of G1 by Th189;
C is Component of G2 by A1, GLIBPRE1:39;
hence x in G2 .allComponents() by Th189; :: thesis: verum

end;

assume x in G2 .allComponents() ; :: thesis: x in G1 .allComponents()
then reconsider C = x as plain Component of G2 by Th189;
C is Component of G1 by A1, GLIBPRE1:39;
hence x in G1 .allComponents() by Th189; :: thesis: verum

end;

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

end;

assume G1 .allComponents() = G2 .allComponents() ; :: thesis: G1 == G2
then ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) by Th193;
hence G1 == G2 by GLIB_000:87; :: thesis: verum