let G be Graph; for p being oriented Chain of G
for U, V being set
for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 holds
p is_orientedpath_of v1,v2,U
let p be oriented Chain of G; for U, V being set
for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 holds
p is_orientedpath_of v1,v2,U
let U, V be set ; for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 holds
p is_orientedpath_of v1,v2,U
let v1, v2 be Vertex of G; ( the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 implies p is_orientedpath_of v1,v2,U )
assume that
A1:
the carrier of G = U \/ V
and
A2:
v1 in U
and
A3:
for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 )
and
A4:
p is_orientedpath_of v1,v2
; p is_orientedpath_of v1,v2,U
set FS = the Source of G;
set FT = the Target of G;
A5:
now vertices p c= Uassume
not
vertices p c= U
;
contradictionthen consider i being
Element of
NAT ,
q,
r being
FinSequence of the
carrier' of
G such that A6:
i + 1
<= len p
and A7:
not
vertices (p /. (i + 1)) c= U
and A8:
len q = i
and A9:
p = q ^ r
and A10:
vertices q c= U
by GRAPH_5:20;
A11:
p . (i + 1) in the
carrier' of
G
by A6, Th2, NAT_1:12;
p /. (i + 1) = p . (i + 1)
by A6, FINSEQ_4:15, NAT_1:12;
then A12:
vertices (p /. (i + 1)) = {( the Source of G . (p . (i + 1))),( the Target of G . (p . (i + 1)))}
by GRAPH_5:def 1;
A14:
1
<= i + 1
by NAT_1:12;
then reconsider vy = the
Target of
G . (p . (i + 1)) as
Vertex of
G by A6, Lm3;
A15:
(
vy in U or
vy in V )
by A1, A2, XBOOLE_0:def 3;
per cases
( i = 0 or i <> 0 )
;
suppose A17:
i <> 0
;
contradictionreconsider vx = the
Source of
G . (p . (i + 1)) as
Vertex of
G by A6, A14, Lm3;
hereby verum
per cases
( vx in U or not vx in U )
;
suppose A19:
not
vx in U
;
contradictionA20:
i < len p
by A6, NAT_1:13;
A21:
i >= 1
+ 0
by A17, INT_1:7;
then reconsider vq = the
Target of
G . (q . i) as
Vertex of
G by A8, Lm3;
A22:
vq in vertices q
by A8, A21, Lm4;
the
Target of
G . (q . i) =
the
Target of
G . (p . i)
by A8, A9, A21, Lm1
.=
the
Source of
G . (p . (i + 1))
by A21, A20, GRAPH_1:def 15
;
hence
contradiction
by A10, A19, A22;
verum end; end; end;
(vertices p) \ {v2} c= vertices p
by XBOOLE_1:36;
then
(vertices p) \ {v2} c= U
by A5;
hence
p is_orientedpath_of v1,v2,U
by A4, GRAPH_5:def 4; verum