let G be Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: p is_orientedpath_of v1,v2,U
set FS = the Source of G;
set FT = the Target of G;

A5: now :: thesis: vertices p c= U

assume not vertices p c= U ; :: thesis: contradiction
then 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;

A13: now :: thesis: ( the Source of G . (p . (i + 1)) in U implies not the Target of G . (p . (i + 1)) in U )

assume ( the Source of G . (p . (i + 1)) in U & the Target of G . (p . (i + 1)) in U ) ; :: thesis: contradiction
then (vertices (p /. (i + 1))) \/ U = U by A12, ZFMISC_1:42;
hence contradiction by A7, XBOOLE_1:7; :: thesis: verum

end;

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 A16: i = 0 ; :: thesis: contradiction

then the Source of G . (p . (i + 1)) = v1 by A4, GRAPH_5:def 3;
then p . (i + 1) orientedly_joins v1,vy by GRAPH_4:def 1;
hence contradiction by A2, A3, A4, A13, A11, A15, A16, GRAPH_5:def 3; :: thesis: verum

end;

suppose A17: i <> 0 ; :: thesis: contradiction

reconsider vx = the Source of G . (p . (i + 1)) as Vertex of G by A6, A14, Lm3;

hereby :: thesis: verum

per cases ( vx in U or not vx in U ) ;

suppose A18: vx in U ; :: thesis: contradiction

p . (i + 1) orientedly_joins vx,vy by GRAPH_4:def 1;
hence contradiction by A3, A6, A14, A13, A15, A18, Th2; :: thesis: verum

end;

suppose A19: not vx in U ; :: thesis: contradiction

A20: 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; :: thesis: verum

end;

end;

end;

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; :: thesis: verum