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

now :: thesis: for x being object holds
( ( not x in G1 .componentSet() or x in (G2 .componentSet()) \ {(G2 .reachableFrom w)} or x in {((G2 .reachableFrom w) \/ {v})} ) & ( ( x in (G2 .componentSet()) \ {(G2 .reachableFrom w)} or x in {((G2 .reachableFrom w) \/ {v})} ) implies x in G1 .componentSet() ) )

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

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

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

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

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

then not v1 in {v} 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 w or v2 in G2 .reachableFrom w ) ;

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

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

end;

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

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

end;

end;

end;

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

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

end;

end;

end;

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

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

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

then A12: ( x in G2 .componentSet() & not x in {(G2 .reachableFrom w)} ) 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 w by A12, TARSKI:def 1;
then x = G1 .reachableFrom v1 by A1, A13, Th56, GLIB_002:12;
hence x in G1 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

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

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

end;

end;

end;

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