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

per cases ( k = len p or k <> len p ) ;

suppose k = len p ; :: thesis: contradiction

then p . k orientedly_joins vx,v2 by A11, GRAPH_4:def 1;
hence contradiction by A3, A4, A9, A10; :: thesis: verum

end;

suppose k <> len p ; :: thesis: contradiction

then A12: k < len p by A9, XXREAL_0:1;
A13: k < k + 1 by NAT_1:13;

A14: now :: thesis: not the Source of G . (p . (k + 1)) in U

assume A15: the Source of G . (p . (k + 1)) in U ; :: thesis: contradiction
( k + 1 <= len p & 1 <= k + 1 ) by A12, INT_1:7, NAT_1:12;
hence contradiction by A9, A13, A15; :: thesis: verum

end;

reconsider vy = the Target of G . (p . k) as Vertex of G by A9, Lm3;
A16: p . k orientedly_joins vx,vy by GRAPH_4:def 1;
the Source of G . (p . (k + 1)) = the Target of G . (p . k) by A9, A12, GRAPH_1:def 15;
then vy in V by A1, A2, A14, XBOOLE_0:def 3;
hence contradiction by A4, A9, A10, A16; :: thesis: verum

end;

end;