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 not e in the_Edges_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( not e in the_Edges_of G2 implies G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} )
assume A1: not e in the_Edges_of G2 ; :: thesis: G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}
set V1 = G2 .reachableFrom v1;
set V2 = G2 .reachableFrom v2;
A2: G2 is Subgraph of G1 by GLIB_006:57;
for x being object holds
( x in G1 .componentSet() iff x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} )

proof

let x be object ; :: thesis: ( x in G1 .componentSet() iff x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} )
reconsider w1 = v1, w2 = v2 as Vertex of G1 by GLIB_006:68;
thus ( x in G1 .componentSet() implies x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} ) :: thesis: ( x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} implies x in G1 .componentSet() )

proof

assume x in G1 .componentSet() ; :: thesis: x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}
then consider w being Vertex of G1 such that
A3: x = G1 .reachableFrom w by GLIB_002:def 8;
reconsider v = w as Vertex of G2 by GLIB_006:102;

per cases ( ( not v in G2 .reachableFrom v1 & not v in G2 .reachableFrom v2 ) or v in G2 .reachableFrom v1 or v in G2 .reachableFrom v2 ) ;

suppose A4: ( not v in G2 .reachableFrom v1 & not v in G2 .reachableFrom v2 ) ; :: thesis: x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}

then A5: G1 .reachableFrom w = G2 .reachableFrom v by A1, Th43;
( G2 .reachableFrom v <> G2 .reachableFrom v1 & G2 .reachableFrom v <> G2 .reachableFrom v2 ) by A4, Th22;
then A6: not G1 .reachableFrom w in {(G2 .reachableFrom v1),(G2 .reachableFrom v2)} by A5, TARSKI:def 2;
G2 .reachableFrom v in G2 .componentSet() by GLIB_002:def 8;
then G1 .reachableFrom w in (G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)} by A5, A6, XBOOLE_0:def 5;
hence x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} by A3, XBOOLE_0:def 3; :: thesis: verum

end;

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

then w in G1 .reachableFrom w1 by A2, TARSKI:def 3, GLIB_002:14;
then x = G1 .reachableFrom w1 by A3, GLIB_002:12
.= (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) by A1, Th42 ;
then x in {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} by TARSKI:def 1;
hence x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} by XBOOLE_0:def 3; :: thesis: verum

end;

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

then w in G1 .reachableFrom w2 by A2, TARSKI:def 3, GLIB_002:14;
then w in G1 .reachableFrom w1 by A1, Th41, GLIB_002:12;
then x = G1 .reachableFrom w1 by A3, GLIB_002:12
.= (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) by A1, Th42 ;
then x in {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} by TARSKI:def 1;
hence x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume x in ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} ; :: thesis: x in G1 .componentSet()

per cases then ( x in (G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)} or x in {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} ) by XBOOLE_0:def 3;

suppose x in (G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)} ; :: thesis: x in G1 .componentSet()

then A7: ( x in G2 .componentSet() & not x in {(G2 .reachableFrom v1),(G2 .reachableFrom v2)} ) by XBOOLE_0:def 5;
then A8: ( x <> G2 .reachableFrom v1 & x <> G2 .reachableFrom v2 ) by TARSKI:def 2;
consider v being Vertex of G2 such that
A9: x = G2 .reachableFrom v by A7, GLIB_002:def 8;
reconsider w = v as Vertex of G1 by GLIB_006:68;
( not v in G2 .reachableFrom v1 & not v in G2 .reachableFrom v2 ) by A8, A9, GLIB_002:12;
then G1 .reachableFrom w = x by A1, A9, Th43;
hence x in G1 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

suppose x in {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} ; :: thesis: x in G1 .componentSet()

then x = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) by TARSKI:def 1;
then x = G1 .reachableFrom w1 by A1, Th42;
hence x in G1 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

end;

end;

hence G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))} by TARSKI:2; :: thesis: verum