let G2 be _Graph; :: thesis:
let v be Vertex of G2; :: thesis:
let e, w be object ; :: thesis:
let G1 be addAdjVertex of G2,v,e,w; :: thesis:
set M1 = (G2 .componentSet()) \ {(G2 .reachableFrom v)};
set M2 = {((G2 .reachableFrom v) \/ {w})};
assume A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) ; :: thesis:
then A2: the_Vertices_of G1 = (the_Vertices_of G2) \/ {w} by GLIB_006:def 12;
then reconsider v9 = v as Vertex of G1 by XBOOLE_0:def 3;
A3: e Joins v,w,G1 by A1, GLIB_006:131;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in G1 .componentSet() ; :: thesis:
then consider v1 being Vertex of G1 such that
A4: x = G1 .reachableFrom v1 by GLIB_002:def 8;

per cases ;

suppose v1 <> w ; :: thesis:

then not v1 in {w} by TARSKI:def 1;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;

per cases ;

suppose not v2 in G2 .reachableFrom v ; :: thesis:

then A5: G2 .reachableFrom v2 misses G2 .reachableFrom v by GLIB_008:22;
then A6: x = G2 .reachableFrom v2 by A1, A4, Th55, GLIB_002:12;
then A7: x in G2 .componentSet() by GLIB_002:def 8;
not x in {(G2 .reachableFrom v)} by A6, A5, TARSKI:def 1;
hence ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) by A7, XBOOLE_0:def 5; :: thesis:

end;

suppose A8: v2 in G2 .reachableFrom v ; :: thesis:

A9: G1 .reachableFrom v9 = (G2 .reachableFrom v) \/ {w} by A1, Th57;
G2 is Subgraph of G1 by GLIB_006:57;
then G2 .reachableFrom v c= G1 .reachableFrom v9 by GLIB_002:14;
then x = (G2 .reachableFrom v) \/ {w} by A4, A8, A9, GLIB_002:12;
hence ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) by TARSKI:def 1; :: thesis:

end;

end;

end;

suppose A10: v1 = w ; :: thesis:

A11: G1 .reachableFrom v9 = (G2 .reachableFrom v) \/ {w} by A1, Th57;
v1 in G1 .reachableFrom v9 by A3, A10, GLIB_002:9, GLIB_002:10;
then x = (G2 .reachableFrom v) \/ {w} by A4, A11, GLIB_002:12;
hence ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) by TARSKI:def 1; :: thesis:

end;

end;

end;

assume ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) ; :: thesis:

per cases ;

suppose x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} ; :: thesis:

then A12: ( x in G2 .componentSet() & not x in {(G2 .reachableFrom v)} ) by XBOOLE_0:def 5;
then consider v2 being Vertex of G2 such that
A13: x = G2 .reachableFrom v2 by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by A2, XBOOLE_0:def 3;
x <> G2 .reachableFrom v by A12, TARSKI:def 1;
then x = G1 .reachableFrom v1 by A1, A13, Th55, GLIB_002:12;
hence x in G1 .componentSet() by GLIB_002:def 8; :: thesis:

end;

suppose x in {((G2 .reachableFrom v) \/ {w})} ; :: thesis:

then A14: x = (G2 .reachableFrom v) \/ {w} by TARSKI:def 1;
G1 .reachableFrom v9 = (G2 .reachableFrom v) \/ {w} by A1, Th57;
hence x in G1 .componentSet() by A14, GLIB_002:def 8; :: thesis:

end;

end;

end;

hence G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})} by XBOOLE_0:def 3; :: thesis: