let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st v2 in G2 .reachableFrom v1 holds
G1 .componentSet() = G2 .componentSet()
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st v2 in G2 .reachableFrom v1 holds
G1 .componentSet() = G2 .componentSet()
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st v2 in G2 .reachableFrom v1 holds
G1 .componentSet() = G2 .componentSet()
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( v2 in G2 .reachableFrom v1 implies G1 .componentSet() = G2 .componentSet() )
assume A1: v2 in G2 .reachableFrom v1 ; :: thesis: G1 .componentSet() = G2 .componentSet()

per cases ( not e in the_Edges_of G2 or e in the_Edges_of G2 ) ;

suppose A2: not e in the_Edges_of G2 ; :: thesis: G1 .componentSet() = G2 .componentSet()

then A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:def 11;
for x being set holds
( x in G2 .componentSet() iff ex v being Vertex of G1 st x = G1 .reachableFrom v )

proof

let x be set ; :: thesis: ( x in G2 .componentSet() iff ex v being Vertex of G1 st x = G1 .reachableFrom v )

hereby :: thesis: ( ex v being Vertex of G1 st x = G1 .reachableFrom v implies x in G2 .componentSet() )

assume x in G2 .componentSet() ; :: thesis: ex v being Vertex of G1 st x = G1 .reachableFrom v
then consider v0 being Vertex of G2 such that
A4: x = G2 .reachableFrom v0 by GLIB_002:def 8;
reconsider v = v0 as Vertex of G1 by A2, GLIB_006:def 11;
take v = v; :: thesis: x = G1 .reachableFrom v
thus x = G1 .reachableFrom v by A1, A4, Th39; :: thesis: verum

end;

given v being Vertex of G1 such that A5: x = G1 .reachableFrom v ; :: thesis: x in G2 .componentSet()
ex v0 being Vertex of G2 st x = G2 .reachableFrom v0

proof

reconsider v0 = v as Vertex of G2 by A2, GLIB_006:def 11;
take v0 ; :: thesis: x = G2 .reachableFrom v0
thus x = G2 .reachableFrom v0 by A1, A5, Th39; :: thesis: verum

end;

hence x in G2 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

hence G1 .componentSet() = G2 .componentSet() by A3, GLIB_002:def 8; :: thesis: verum

end;

suppose e in the_Edges_of G2 ; :: thesis: G1 .componentSet() = G2 .componentSet()

then G1 == G2 by GLIB_006:def 11;
hence G1 .componentSet() = G2 .componentSet() by GLIB_002:26; :: thesis: verum

end;

end;