let G1 be non _trivial _Graph; for v0, v1 being Vertex of G1
for G2 being removeVertex of G1,v0
for v2 being Vertex of G2 st v1 = v2 & not v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = G1 .reachableFrom v1
let v0, v1 be Vertex of G1; for G2 being removeVertex of G1,v0
for v2 being Vertex of G2 st v1 = v2 & not v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = G1 .reachableFrom v1
let G2 be removeVertex of G1,v0; for v2 being Vertex of G2 st v1 = v2 & not v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = G1 .reachableFrom v1
let v2 be Vertex of G2; ( v1 = v2 & not v1 in G1 .reachableFrom v0 implies G2 .reachableFrom v2 = G1 .reachableFrom v1 )
assume A1:
( v1 = v2 & not v1 in G1 .reachableFrom v0 )
; G2 .reachableFrom v2 = G1 .reachableFrom v1
then A2:
G2 .reachableFrom v2 c= G1 .reachableFrom v1
by GLIB_002:14;
for w being object st w in G1 .reachableFrom v1 holds
w in G2 .reachableFrom v2
proof
let w be
object ;
( w in G1 .reachableFrom v1 implies w in G2 .reachableFrom v2 )
assume
w in G1 .reachableFrom v1
;
w in G2 .reachableFrom v2
then consider W being
Walk of
G1 such that A3:
W is_Walk_from v1,
w
by GLIB_002:def 5;
not
v0 in W .vertices()
proof
assume A4:
v0 in W .vertices()
;
contradiction
reconsider m = 1 as
odd Element of
NAT by POLYFORM:4;
reconsider n =
W .find v0 as
odd Element of
NAT ;
set U =
W .cut (
m,
n);
(
m <= n &
n <= len W )
by A4, GLIB_001:def 19, CHORD:2;
then
W .cut (
m,
n)
is_Walk_from W . m,
W . n
by GLIB_001:37;
then
W .cut (
m,
n)
is_Walk_from W .first() ,
W . n
by GLIB_001:def 6;
then
W .cut (
m,
n)
is_Walk_from v1,
W . n
by A3, GLIB_001:def 23;
then
W .cut (
m,
n)
is_Walk_from v1,
v0
by A4, GLIB_001:def 19;
then
(W .cut (m,n)) .reverse() is_Walk_from v0,
v1
by GLIB_001:23;
hence
contradiction
by A1, GLIB_002:def 5;
verum
end;
then reconsider W2 =
W as
Walk of
G2 by GLIB_001:171;
W2 is_Walk_from v2,
w
by A1, A3, GLIB_001:19;
hence
w in G2 .reachableFrom v2
by GLIB_002:def 5;
verum
end;
then
G1 .reachableFrom v1 c= G2 .reachableFrom v2
by TARSKI:def 3;
hence
G2 .reachableFrom v2 = G1 .reachableFrom v1
by A2, XBOOLE_0:def 10; verum