let G2 be _Graph; for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1
for v being Vertex of G2 st v2 in G2 .reachableFrom v1 & v = w holds
G1 .reachableFrom w = G2 .reachableFrom v
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1
for v being Vertex of G2 st v2 in G2 .reachableFrom v1 & v = w holds
G1 .reachableFrom w = G2 .reachableFrom v
let e be object ; for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1
for v being Vertex of G2 st v2 in G2 .reachableFrom v1 & v = w holds
G1 .reachableFrom w = G2 .reachableFrom v
let G1 be addEdge of G2,v1,e,v2; for w being Vertex of G1
for v being Vertex of G2 st v2 in G2 .reachableFrom v1 & v = w holds
G1 .reachableFrom w = G2 .reachableFrom v
let w be Vertex of G1; for v being Vertex of G2 st v2 in G2 .reachableFrom v1 & v = w holds
G1 .reachableFrom w = G2 .reachableFrom v
let v be Vertex of G2; ( v2 in G2 .reachableFrom v1 & v = w implies G1 .reachableFrom w = G2 .reachableFrom v )
assume that
A1:
v2 in G2 .reachableFrom v1
and
A2:
w = v
; G1 .reachableFrom w = G2 .reachableFrom v
per cases
( not e in the_Edges_of G2 or e in the_Edges_of G2 )
;
suppose A3:
not
e in the_Edges_of G2
;
G1 .reachableFrom w = G2 .reachableFrom v
G2 is
Subgraph of
G1
by GLIB_006:57;
then A4:
G2 .reachableFrom v c= G1 .reachableFrom w
by A2, GLIB_002:14;
for
y being
object st
y in G1 .reachableFrom w holds
y in G2 .reachableFrom v
proof
let y be
object ;
( y in G1 .reachableFrom w implies y in G2 .reachableFrom v )
assume
y in G1 .reachableFrom w
;
y in G2 .reachableFrom v
then consider W1 being
Walk of
G1 such that A5:
W1 is_Walk_from w,
y
by GLIB_002:def 5;
set T = the
Trail of
W1;
y is
set
by TARSKI:1;
then A6:
the
Trail of
W1 is_Walk_from w,
y
by A5, GLIB_001:160;
per cases
( not e in the Trail of W1 .edges() or e in the Trail of W1 .edges() )
;
suppose
e in the
Trail of
W1 .edges()
;
y in G2 .reachableFrom vthen consider w1,
w2 being
Vertex of
G1,
n being
odd Element of
NAT such that A7:
n + 2
<= len the
Trail of
W1
and A8:
(
w1 = the
Trail of
W1 . n &
e = the
Trail of
W1 . (n + 1) &
w2 = the
Trail of
W1 . (n + 2) )
and A9:
e Joins w1,
w2,
G1
by GLIB_001:103;
set E =
G1 .walkOf (
w1,
e,
w2);
A10:
G1 .walkOf (
w1,
e,
w2)
is_odd_substring_of the
Trail of
W1,
0
by A7, A8, GLIB_006:27;
e DJoins v1,
v2,
G1
by A3, GLIB_006:105;
then A11:
e Joins v1,
v2,
G1
by GLIB_000:16;
per cases then
( ( v1 = w1 & v2 = w2 ) or ( v1 = w2 & v2 = w1 ) )
by A9, GLIB_000:15;
suppose A12:
(
v1 = w1 &
v2 = w2 )
;
y in G2 .reachableFrom vconsider W2 being
Walk of
G2 such that A13:
W2 is_Walk_from v1,
v2
by A1, GLIB_002:def 5;
reconsider W4 =
W2 as
Walk of
G1 by GLIB_006:75;
not
e in W2 .edges()
by A3;
then A14:
not
e in W4 .edges()
by GLIB_001:110;
set W5 = the
Trail of
W1 .replaceEdgeWith (
e,
W4);
A15:
the
Trail of
W1 .replaceEdgeWith (
e,
W4)
is_Walk_from v,
y
by A2, A6, GLIB_006:47;
(
W2 .first() = v1 &
W2 .last() = v2 )
by A13, GLIB_001:def 23;
then
(
W4 .first() = v1 &
W4 .last() = v2 )
by GLIB_001:16;
then
not
e in ( the Trail of W1 .replaceEdgeWith (e,W4)) .edges()
by A11, A14, GLIB_006:40, A10, A12;
then reconsider W = the
Trail of
W1 .replaceEdgeWith (
e,
W4) as
Walk of
G2 by GLIB_006:109;
W is_Walk_from v,
y
by A15, GLIB_001:19;
hence
y in G2 .reachableFrom v
by GLIB_002:def 5;
verum end; suppose A17:
(
v1 = w2 &
v2 = w1 )
;
y in G2 .reachableFrom vconsider W3 being
Walk of
G2 such that A18:
W3 is_Walk_from v1,
v2
by A1, GLIB_002:def 5;
A19:
W3 .reverse() is_Walk_from v2,
v1
by A18, GLIB_001:23;
reconsider W4 =
W3 .reverse() as
Walk of
G1 by GLIB_006:75;
not
e in (W3 .reverse()) .edges()
by A3;
then A20:
not
e in W4 .edges()
by GLIB_001:110;
set W5 = the
Trail of
W1 .replaceEdgeWith (
e,
W4);
A21:
the
Trail of
W1 .replaceEdgeWith (
e,
W4)
is_Walk_from v,
y
by A2, A6, GLIB_006:47;
(
(W3 .reverse()) .first() = v2 &
(W3 .reverse()) .last() = v1 )
by A19, GLIB_001:def 23;
then
(
W4 .first() = v2 &
W4 .last() = v1 )
by GLIB_001:16;
then
not
e in ( the Trail of W1 .replaceEdgeWith (e,W4)) .edges()
by A11, A20, GLIB_006:40, GLIB_000:14, A10, A17;
then reconsider W = the
Trail of
W1 .replaceEdgeWith (
e,
W4) as
Walk of
G2 by GLIB_006:109;
W is_Walk_from v,
y
by A21, GLIB_001:19;
hence
y in G2 .reachableFrom v
by GLIB_002:def 5;
verum end; end;
end; then
G1 .reachableFrom w c= G2 .reachableFrom v
by TARSKI:def 3;
hence
G1 .reachableFrom w = G2 .reachableFrom v
by A4, XBOOLE_0:def 10;
verum end;