let V be set ; for G being Graph
for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element of G
for p, q being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds
q is_orientedpath_of v1,v3,V \/ {v2}
let G be Graph; for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element of G
for p, q being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds
q is_orientedpath_of v1,v3,V \/ {v2}
let pe be FinSequence of the carrier' of G; for v1, v2, v3 being Element of G
for p, q being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds
q is_orientedpath_of v1,v3,V \/ {v2}
let v1, v2, v3 be Element of G; for p, q being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds
q is_orientedpath_of v1,v3,V \/ {v2}
let p, q be oriented Chain of G; ( q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 implies q is_orientedpath_of v1,v3,V \/ {v2} )
assume that
A1:
q = p ^ pe
and
A2:
( len p >= 1 & len pe = 1 )
and
A3:
p is_orientedpath_of v1,v2,V
and
A4:
pe . 1 orientedly_joins v2,v3
; q is_orientedpath_of v1,v3,V \/ {v2}
p is_orientedpath_of v1,v2
by A3;
then A5:
ex r being oriented Chain of G st
( r = p ^ pe & r is_orientedpath_of v1,v3 )
by A2, A4, Th31;
set FT = the Target of G;
the Target of G . (pe . 1) = v3
by A4, GRAPH_4:def 1;
then (vertices q) \ {v3} =
((vertices p) \/ {v3}) \ {v3}
by A1, A2, Th25
.=
(vertices p) \ {v3}
by XBOOLE_1:40
;
then A6:
(vertices q) \ {v3} c= vertices p
by XBOOLE_1:36;
(vertices p) \ {v2} c= V
by A3;
then
vertices p c= V \/ {v2}
by XBOOLE_1:44;
then
(vertices q) \ {v3} c= V \/ {v2}
by A6;
hence
q is_orientedpath_of v1,v3,V \/ {v2}
by A1, A5; verum