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_{1}[ Nat] means ( $1 >= 1 & $1 <= len p & the Source of G . (p . $1) in U );

A7: for k being Nat st S_{1}[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_{1}[k]
by A2, A6;

consider k being Nat such that

A9: ( S_{1}[k] & ( for n being Nat st S_{1}[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;

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

A7: for k being Nat st S

k <= len p ;

the Source of G . (p . 1) = v1 by A5, GRAPH_5:def 3;

then A8: ex k being Nat st S

consider k being Nat such that

A9: ( S

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 )
;

end;

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;hence contradiction by A3, A4, A9, A10; :: thesis: verum

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

then A12:
k < len p
by A9, XXREAL_0:1;

A13: k < k + 1 by NAT_1:13;

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;A13: k < k + 1 by NAT_1:13;

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

reconsider vy = the Target of G . (p . k) as Vertex of G by A9, Lm3;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;( k + 1 <= len p & 1 <= k + 1 ) by A12, INT_1:7, NAT_1:12;

hence contradiction by A9, A13, A15; :: thesis: verum

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