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 A1: ( 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 ) ; :: thesis: p is_orientedpath_of v1,v2,U
set FS = the Source of G;
set FT = the Target of G;
A2: (vertices p) \ {v2} c= vertices p by XBOOLE_1:36;

now

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
A3: ( i + 1 <= len p & not vertices (p /. (i + 1)) c= U & len q = i & p = q ^ r & vertices q c= U ) by GRAPH_5:23;
A4: 1 <= i + 1 by NAT_1:12;
p /. (i + 1) = p . (i + 1) by A3, FINSEQ_4:24, NAT_1:12;
then A5: vertices (p /. (i + 1)) = {(the Source of G . (p . (i + 1))),(the Target of G . (p . (i + 1)))} by GRAPH_5:def 1;

A6: now

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 A5, ZFMISC_1:48;
hence contradiction by A3, XBOOLE_1:7; :: thesis: verum

end;

A7: p . (i + 1) in the carrier' of G by A3, Th2, NAT_1:12;
reconsider vy = the Target of G . (p . (i + 1)) as Vertex of G by A3, A4, Lm3;
A9: ( vy in U or vy in V ) by A1, XBOOLE_0:def 3;

per cases ( i = 0 or i <> 0 ) ;

suppose A10: i = 0 ; :: thesis: contradiction

then the Source of G . (p . (i + 1)) = v1 by A1, GRAPH_5:def 3;
then p . (i + 1) orientedly_joins v1,vy by GRAPH_4:def 1;
hence contradiction by A1, A6, A7, A9, A10, GRAPH_5:def 3; :: thesis: verum

end;

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

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

hereby :: thesis: verum

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

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

p . (i + 1) orientedly_joins vx,vy by GRAPH_4:def 1;
hence contradiction by A1, A3, A4, A6, A9, A12, Th2; :: thesis: verum

end;

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

i > 0 by A11;
then A14: i >= 1 + 0 by INT_1:20;
then reconsider vq = the Target of G . (q . i) as Vertex of G by A3, Lm3;
A15: vq in vertices q by A3, A14, Lm4;
A16: i < len p by A3, NAT_1:13;
the Target of G . (q . i) = the Target of G . (p . i) by A3, A14, Lm1
.= the Source of G . (p . (i + 1)) by A14, A16, GRAPH_1:def 13 ;
hence contradiction by A3, A13, A15; :: thesis: verum

end;

end;

end;

end;

end;

end;

then (vertices p) \ {v2} c= U by A2, XBOOLE_1:1;
hence p is_orientedpath_of v1,v2,U by A1, GRAPH_5:def 4; :: thesis: verum