let G be Graph; :: thesis:
let U, V be set ; :: thesis:
let v1, v2 be Vertex of G; :: thesis:
assume A1: ( the carrier of G = U \/ V & v1 in U & v2 in V & ( 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 ) ) ) ; :: thesis:
given p being oriented Chain of G such that A2: p is_orientedpath_of v1,v2 ; :: thesis:
set FS = the Source of G;
set FT = the Target of G;
A3: ( p <> {} & the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by A2, GRAPH_5:def 3;
then A4: len p >= 1 by FINSEQ_1:28;
defpred S₁[ Nat] means ( $1 >= 1 & $1 <= len p & the Source of G . (p . $1) in U );
A5: for k being Nat st S₁[k] holds
k <= len p ;
A6: ex k being Nat st S₁[k] by A1, A3, A4;
consider k being Nat such that
A7: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A5, A6);
reconsider k = k as Element of NAT by ORDINAL1:def 13;
reconsider vx = the Source of G . (p . k) as Vertex of G by A7, Lm3;
A8: p . k in the carrier' of G by A7, Th2;

per cases ;

suppose k = len p ; :: thesis:

then p . k orientedly_joins vx,v2 by A3, GRAPH_4:def 1;
hence contradiction by A1, A7, A8; :: thesis:

end;

suppose k <> len p ; :: thesis:

then A9: k < len p by A7, XXREAL_0:1;
then A10: the Source of G . (p . (k + 1)) = the Target of G . (p . k) by A7, GRAPH_1:def 13;
A11: k < k + 1 by NAT_1:13;

A12: now

assume A13: the Source of G . (p . (k + 1)) in U ; :: thesis:
A14: k + 1 <= len p by A9, INT_1:20;
1 <= k + 1 by NAT_1:12;
hence contradiction by A7, A11, A13, A14; :: thesis:

end;

reconsider vy = the Target of G . (p . k) as Vertex of G by A7, Lm3;
A16: vy in V by A1, A10, A12, XBOOLE_0:def 3;
p . k orientedly_joins vx,vy by GRAPH_4:def 1;
hence contradiction by A1, A7, A8, A16; :: thesis:

end;