let G1 be _Graph; :: thesis: for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds
G1 .componentSet() = G2 .componentSet()
let G2 be spanning Subgraph of G1; :: thesis: ( ( for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ) implies G1 .componentSet() = G2 .componentSet() )
assume A1: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ; :: thesis: G1 .componentSet() = G2 .componentSet()
for C being object holds
( C in G1 .componentSet() iff C in G2 .componentSet() )

proof

let C be object ; :: thesis: ( C in G1 .componentSet() iff C in G2 .componentSet() )

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

assume C in G1 .componentSet() ; :: thesis: C in G2 .componentSet()
then consider v1 being Vertex of G1 such that
A2: C = G1 .reachableFrom v1 by GLIB_002:def 8;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:def 33;
C = G2 .reachableFrom v2 by A1, A2;
hence C in G2 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

assume C in G2 .componentSet() ; :: thesis: C in G1 .componentSet()
then consider v2 being Vertex of G2 such that
A3: C = G2 .reachableFrom v2 by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by GLIB_000:def 33;
C = G1 .reachableFrom v1 by A1, A3;
hence C in G1 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

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