let G2 be _Graph; for w, v2 being Vertex of G2
for v, e being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = v2 & not w in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let w, v2 be Vertex of G2; for v, e being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = v2 & not w in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let v, e be object ; for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = v2 & not w in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let G1 be addAdjVertex of G2,v,e,w; for v1 being Vertex of G1 st v1 = v2 & not w in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
let v1 be Vertex of G1; ( v1 = v2 & not w in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 implies G1 .reachableFrom v1 = G2 .reachableFrom v2 )
assume that
A1:
( v1 = v2 & not w in G2 .reachableFrom v2 )
and
A2:
( not e in the_Edges_of G2 & not v in the_Vertices_of G2 )
; G1 .reachableFrom v1 = G2 .reachableFrom v2
A3:
G2 is Subgraph of G1
by GLIB_006:57;
then A4:
G2 .reachableFrom v2 c= G1 .reachableFrom v1
by A1, GLIB_002:14;
now for x being object st x in G1 .reachableFrom v1 holds
x in G2 .reachableFrom v2let x be
object ;
( x in G1 .reachableFrom v1 implies x in G2 .reachableFrom v2 )assume
x in G1 .reachableFrom v1
;
x in G2 .reachableFrom v2then consider W1 being
Walk of
G1 such that A5:
W1 is_Walk_from v1,
x
by GLIB_002:def 5;
set P1 = the
Path of
W1;
x is
set
by TARSKI:1;
then A6:
the
Path of
W1 is_Walk_from v1,
x
by A5, GLIB_001:160;
then A7:
( the
Path of
W1 .first() = v1 & the
Path of
W1 .last() = x )
by GLIB_001:def 23;
A8:
x <> v
proof
per cases
( not the Path of W1 is trivial or not the Path of W1 is trivial )
;
suppose
the
Path of
W1 is
trivial
;
x <> vthen A9:
3
<= len the
Path of
W1
by GLIB_001:125;
then
( 3
- 3
<= (len the Path of W1) - 2 &
(len the Path of W1) - 2
< (len the Path of W1) - 0 )
by XREAL_1:10, XREAL_1:13;
then A10:
(
(len the Path of W1) - 2
in NAT &
(len the Path of W1) - 2
< len the
Path of
W1 )
by INT_1:3;
then reconsider m =
(len the Path of W1) - 2 as
odd Element of
NAT by POLYFORM:5;
the
Path of
W1 . (m + 1) Joins the
Path of
W1 . m, the
Path of
W1 . (m + 2),
G1
by A10, GLIB_001:def 3;
then
the
Path of
W1 . (m + 1) Joins the
Path of
W1 . m,
x,
G1
by A7;
then A11:
the
Path of
W1 . (m + 1) Joins x, the
Path of
W1 . m,
G1
by GLIB_000:14;
assume
x = v
;
contradictionthen A12:
the
Path of
W1 . m = w
by A2, A11, GLIB_006:134;
set P2 = the
Path of
W1 .cut (1,
m);
( 3
- 2
<= m &
m <= (len the Path of W1) - 0 )
by A9, XREAL_1:9, XREAL_1:10;
then
(
( the Path of W1 .cut (1,m)) .first() = the
Path of
W1 . 1 &
( the Path of W1 .cut (1,m)) .last() = the
Path of
W1 . m )
by GLIB_001:37, POLYFORM:4;
then A13:
(
( the Path of W1 .cut (1,m)) .first() = v2 &
( the Path of W1 .cut (1,m)) .last() = w )
by A1, A7, A12;
v2 <> w
by A1, GLIB_002:9;
then A14:
the
Path of
W1 .cut (1,
m) is
trivial
by A13, GLIB_001:127;
not
e in ( the Path of W1 .cut (1,m)) .edges()
by A2, A13, GLIB_006:147;
then reconsider P2 = the
Path of
W1 .cut (1,
m) as
Walk of
G2 by A2, A14, GLIB_006:146;
(
P2 .first() = v2 &
P2 .last() = w )
by A13;
then
P2 is_Walk_from v2,
w
by GLIB_001:def 23;
hence
contradiction
by A1, GLIB_002:def 5;
verum end;
end;
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v}
by A2, GLIB_006:def 12;
then
(
x in the_Vertices_of G2 or
x in {v} )
by A7, XBOOLE_0:def 3;
then A15:
not
e in the
Path of
W1 .edges()
by A1, A2, A7, A8, TARSKI:def 1, GLIB_006:147;
the
Path of
W1 is
Walk of
G2
then reconsider P2 = the
Path of
W1 as
Walk of
G2 ;
P2 is_Walk_from v2,
x
by A1, A6, GLIB_001:19;
hence
x in G2 .reachableFrom v2
by GLIB_002:def 5;
verum end;
then
G1 .reachableFrom v1 c= G2 .reachableFrom v2
by TARSKI:def 3;
hence
G1 .reachableFrom v1 = G2 .reachableFrom v2
by A4, XBOOLE_0:def 10; verum