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 w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 holds
G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
let v1, v2 be Vertex of G2; for e being object
for G1 being addEdge of G2,v1,e,v2
for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 holds
G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
let e be object ; for G1 being addEdge of G2,v1,e,v2
for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 holds
G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
let G1 be addEdge of G2,v1,e,v2; for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 holds
G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
let w1 be Vertex of G1; ( not e in the_Edges_of G2 & w1 = v1 implies G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) )
assume A1:
( not e in the_Edges_of G2 & w1 = v1 )
; G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
A2:
G2 is Subgraph of G1
by GLIB_006:57;
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 w1 holds
x in (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
proof
let x be
object ;
( x in G1 .reachableFrom w1 implies x in (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) )
assume A4:
x in G1 .reachableFrom w1
;
x in (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
per cases
( x = w1 or x <> w1 )
;
suppose A5:
x <> w1
;
x in (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)consider W1 being
Walk of
G1 such that A6:
W1 is_Walk_from w1,
x
by A4, GLIB_002:def 5;
set P1 = the
Path of
W1 .reverse() ;
A7:
W1 .reverse() is_Walk_from x,
w1
by A6, GLIB_001:23;
x is
set
by TARSKI:1;
then A8:
the
Path of
W1 .reverse() is_Walk_from x,
w1
by A7, GLIB_001:160;
per cases
( not e in the Path of W1 .reverse() .edges() or e in the Path of W1 .reverse() .edges() )
;
suppose
e in the
Path of
W1 .reverse() .edges()
;
x in (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)then consider u1,
u2 being
Vertex of
G1,
n being
odd Element of
NAT such that A9:
(
n + 2
<= len the
Path of
W1 .reverse() &
u1 = the
Path of
W1 .reverse() . n &
e = the
Path of
W1 .reverse() . (n + 1) &
u2 = the
Path of
W1 .reverse() . (n + 2) )
and A10:
e Joins u1,
u2,
G1
by GLIB_001:103;
A11:
(
v2 = u1 &
v1 = u2 )
proof
assume
( not
v2 = u1 or not
v1 = u2 )
;
contradiction
then A12:
v1 = the
Path of
W1 .reverse() . n
by A3, A9, A10, GLIB_000:15;
A13: the
Path of
W1 .reverse() . (len the Path of W1 .reverse() ) =
the
Path of
W1 .reverse() .last()
by GLIB_001:def 7
.=
v1
by A1, A8, GLIB_001:def 23
;
(n + 2) - 2
< (len the Path of W1 .reverse() ) - 0
by A9, XREAL_1:15;
then
n = 1
by A12, A13, GLIB_001:def 28;
then v1 =
the
Path of
W1 .reverse() .first()
by A12, GLIB_001:def 6
.=
x
by A8, GLIB_001:def 23
;
hence
contradiction
by A1, A5;
verum
end; set P2 = the
Path of
W1 .reverse() .cut (1,
n);
not
e in ( the Path of W1 .reverse() .cut (1,n)) .edges()
proof
assume
e in ( the Path of W1 .reverse() .cut (1,n)) .edges()
;
contradiction
then consider u3,
u4 being
Vertex of
G1,
m being
odd Element of
NAT such that A14:
(
m + 2
<= len ( the Path of W1 .reverse() .cut (1,n)) &
u3 = ( the Path of W1 .reverse() .cut (1,n)) . m &
e = ( the Path of W1 .reverse() .cut (1,n)) . (m + 1) &
u4 = ( the Path of W1 .reverse() .cut (1,n)) . (m + 2) )
and
e Joins u3,
u4,
G1
by GLIB_001:103;
(n + 2) - 2
<= (len the Path of W1 .reverse() ) - 0
by A9, XREAL_1:13;
then A15:
( 1
<= n &
n <= len the
Path of
W1 .reverse() )
by ABIAN:12;
A16:
(m + 2) - 2
< (len ( the Path of W1 .reverse() .cut (1,n))) - 0
by A14, XREAL_1:15;
then A17:
the
Path of
W1 .reverse() . (m + 1) = the
Path of
W1 .reverse() . (n + 1)
by A9, A14, A15, POLYFORM:4, GLIB_001:36;
A18:
( 1
+ 0 <= m + 1 &
m < n )
by A15, A16, GLIB_001:45, XREAL_1:7;
then A19:
m + 1
< n + 1
by XREAL_1:6;
(n + 2) - 1
<= (len the Path of W1 .reverse() ) - 0
by A9, XREAL_1:13;
hence
contradiction
by A17, A18, A19, GLIB_001:138;
verum
end; then reconsider W2 = the
Path of
W1 .reverse() .cut (1,
n) as
Walk of
G2 by GLIB_006:109;
(n + 2) - 2
<= (len the Path of W1 .reverse() ) - 0
by A9, XREAL_1:13;
then
( 1
<= n &
n <= len the
Path of
W1 .reverse() )
by ABIAN:12;
then
the
Path of
W1 .reverse() .cut (1,
n)
is_Walk_from the
Path of
W1 .reverse() . 1, the
Path of
W1 .reverse() . n
by POLYFORM:4, GLIB_001:37;
then
W2 is_Walk_from the
Path of
W1 .reverse() . 1, the
Path of
W1 .reverse() . n
by GLIB_001:19;
then
W2 is_Walk_from the
Path of
W1 .reverse() .first() , the
Path of
W1 .reverse() . n
by GLIB_001:def 6;
then
W2 is_Walk_from x,
v2
by A8, A9, A11, GLIB_001:def 23;
then
W2 .reverse() is_Walk_from v2,
x
by GLIB_001:23;
then
x in G2 .reachableFrom v2
by GLIB_002:def 5;
hence
x in (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
by XBOOLE_0:def 3;
verum end; end;
end;
then A20:
G1 .reachableFrom w1 c= (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
by TARSKI:def 3;
A21:
G2 .reachableFrom v1 c= G1 .reachableFrom w1
by A1, A2, GLIB_002:14;
reconsider w2 = v2 as Vertex of G1 by GLIB_006:68;
G2 .reachableFrom v2 c= G1 .reachableFrom w2
by A2, GLIB_002:14;
then
G2 .reachableFrom v2 c= G1 .reachableFrom w1
by A1, Th41, GLIB_002:12;
then
(G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) c= G1 .reachableFrom w1
by A21, XBOOLE_1:8;
hence
G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
by A20, XBOOLE_0:def 10; verum