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
for w1, w2 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 & w2 = v2 holds
w2 in G1 .reachableFrom w1
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2
for w1, w2 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 & w2 = v2 holds
w2 in G1 .reachableFrom w1
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2
for w1, w2 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 & w2 = v2 holds
w2 in G1 .reachableFrom w1
let G1 be addEdge of G2,v1,e,v2; :: thesis: for w1, w2 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 & w2 = v2 holds
w2 in G1 .reachableFrom w1
let w1, w2 be Vertex of G1; :: thesis: ( not e in the_Edges_of G2 & w1 = v1 & w2 = v2 implies w2 in G1 .reachableFrom w1 )
assume that
A1: not e in the_Edges_of G2 and
A2: ( w1 = v1 & w2 = v2 ) ; :: thesis: w2 in G1 .reachableFrom w1
e DJoins v1,v2,G1 by A1, GLIB_006:105;
then e Joins w1,v2,G1 by A2, GLIB_000:16;
then G1 .walkOf (w1,e,w2) is_Walk_from w1,w2 by A2, GLIB_001:15;
hence w2 in G1 .reachableFrom w1 by GLIB_002:def 5; :: thesis: verum