let G be Graph; 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 ; 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; ( 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 )
; 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
; contradiction
p <> {}
by A5, GRAPH_5:def 3;
then A6:
len p >= 1
by FINSEQ_1:20;
defpred S1[ Nat] means ( $1 >= 1 & $1 <= len p & the Source of G . (p . $1) in U );
A7:
for k being Nat st S1[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 S1[k]
by A2, A6;
consider k being Nat such that
A9:
( S1[k] & ( for n being Nat st S1[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
;
contradictionthen A12:
k < len p
by A9, XXREAL_0:1;
A13:
k < k + 1
by NAT_1:13;
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;
verum end;