let G2 be _Graph; :: thesis:
let v1, v2 be Vertex of G2; :: thesis:
let e be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
let w be Vertex of G1; :: thesis:
let v be Vertex of G2; :: thesis:
assume that
A1: ( not e in the_Edges_of G2 & v = w ) and
A2: ( not v in G2 .reachableFrom v1 & not v in G2 .reachableFrom v2 ) ; :: thesis:
e DJoins v1,v2,G1 by A1, GLIB_006:105;
then A3: e Joins v1,v2,G1 by GLIB_000:16;
for x being object st x in G1 .reachableFrom w holds
x in G2 .reachableFrom v

proof

let x be object ; :: thesis:
assume x in G1 .reachableFrom w ; :: thesis:
then consider W1 being Walk of G1 such that
A4: W1 is_Walk_from w,x by GLIB_002:def 5;
set T1 = the Trail of W1;
x is set by TARSKI:1;
then A5: the Trail of W1 is_Walk_from w,x by A4, GLIB_001:160;
not e in the Trail of W1 .edges()

proof

assume e in the Trail of W1 .edges() ; :: thesis:
then consider u1, u2 being Vertex of G1, n being odd Element of NAT such that
A6: ( n + 2 <= len the Trail of W1 & u1 = the Trail of W1 . n & e = the Trail of W1 . (n + 1) & u2 = the Trail of W1 . (n + 2) ) and
A7: e Joins u1,u2,G1 by GLIB_001:103;
set T2 = the Trail of W1 .cut (1,n);
(n + 2) - 2 <= (len the Trail of W1) - 0 by A6, XREAL_1:13;
then A8: ( 1 <= n & n <= len the Trail of W1 ) by ABIAN:12;
not e in ( the Trail of W1 .cut (1,n)) .edges()

proof

assume e in ( the Trail of W1 .cut (1,n)) .edges() ; :: thesis:
then consider u3, u4 being Vertex of G1, m being odd Element of NAT such that
A9: ( m + 2 <= len ( the Trail of W1 .cut (1,n)) & u3 = ( the Trail of W1 .cut (1,n)) . m & e = ( the Trail of W1 .cut (1,n)) . (m + 1) & u4 = ( the Trail of W1 .cut (1,n)) . (m + 2) ) and
e Joins u3,u4,G1 by GLIB_001:103;
A10: (m + 2) - 2 < (len ( the Trail of W1 .cut (1,n))) - 0 by A9, XREAL_1:15;
then A11: the Trail of W1 . (m + 1) = the Trail of W1 . (n + 1) by A6, A9, A8, POLYFORM:4, GLIB_001:36;
A12: ( 1 + 0 <= m + 1 & m < n ) by A8, A10, XREAL_1:7, GLIB_001:45;
then A13: m + 1 < n + 1 by XREAL_1:6;
(n + 2) - 1 <= (len the Trail of W1) - 0 by A6, XREAL_1:13;
hence contradiction by A11, A12, A13, GLIB_001:138; :: thesis:

end;

then reconsider W2 = the Trail of W1 .cut (1,n) as Walk of G2 by GLIB_006:109;
the Trail of W1 .cut (1,n) is_Walk_from the Trail of W1 . 1, the Trail of W1 . n by A8, POLYFORM:4, GLIB_001:37;
then the Trail of W1 .cut (1,n) is_Walk_from the Trail of W1 .first() , the Trail of W1 . n by GLIB_001:def 6;
then the Trail of W1 .cut (1,n) is_Walk_from w, the Trail of W1 . n by A5, GLIB_001:def 23;
then A14: W2 is_Walk_from v,u1 by A1, A6, GLIB_001:19;

per cases by A3, A7, GLIB_000:15;

suppose ( v1 = u1 & v2 = u2 ) ; :: thesis:

then W2 .reverse() is_Walk_from v1,v by A14, GLIB_001:23;
hence contradiction by A2, GLIB_002:def 5; :: thesis:

end;

suppose ( v1 = u2 & v2 = u1 ) ; :: thesis:

then W2 .reverse() is_Walk_from v2,v by A14, GLIB_001:23;
hence contradiction by A2, GLIB_002:def 5; :: thesis:

end;

end;

end;

then reconsider W = the Trail of W1 as Walk of G2 by GLIB_006:109;
W is_Walk_from w,x by A5, GLIB_001:19;
hence x in G2 .reachableFrom v by A1, GLIB_002:def 5; :: thesis:

end;

then A15: G1 .reachableFrom w c= G2 .reachableFrom v by TARSKI:def 3;
G2 is Subgraph of G1 by GLIB_006:57;
then G2 .reachableFrom v c= G1 .reachableFrom w by A1, GLIB_002:14;
hence G1 .reachableFrom w = G2 .reachableFrom v by A15, XBOOLE_0:def 10; :: thesis: