let G2 be _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})}
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})}
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})}
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 implies G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})} )
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: G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})}
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: for x being object holds
( ( not x in G1 .componentSet() or x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) & ( ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) implies x in G1 .componentSet() ) )

let x be object ; :: thesis: ( ( not x in G1 .componentSet() or x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) & ( ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) implies b₁ in G1 .componentSet() ) )

hereby :: thesis: ( ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) implies b₁ in G1 .componentSet() )

assume x in G1 .componentSet() ; :: thesis: ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} )
then consider v1 being Vertex of G1 such that
A4: x = G1 .reachableFrom v1 by GLIB_002:def 8;

per cases ( v1 <> w or v1 = w ) ;

suppose v1 <> w ; :: thesis: ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} )

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 ( not v2 in G2 .reachableFrom v or v2 in G2 .reachableFrom v ) ;

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

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: verum

end;

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

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: verum

end;

end;

end;

suppose A10: v1 = w ; :: thesis: ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} )

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: verum

end;

end;

end;

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

per cases then ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v)} or x in {((G2 .reachableFrom v) \/ {w})} ) ;

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

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: verum

end;

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

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: verum

end;

end;

end;

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