let G1 be _Graph; :: thesis:
let G2 be spanning Subgraph of G1; :: thesis:
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:
for C being object holds
( C in G1 .componentSet() iff C in G2 .componentSet() )

proof

let C be object ; :: thesis:

hereby :: thesis:

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

end;

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

end;

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