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() )

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

hence
G1 .componentSet() = G2 .componentSet()
by TARSKI:2; :: thesis: verum
let C be object ; :: thesis: ( C in G1 .componentSet() iff C in G2 .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;hereby :: thesis: ( C in G2 .componentSet() implies C in G1 .componentSet() )

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

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