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 that

A1: the carrier of G = U \/ V and

A2: v1 in U and

A3: 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 ) and

A4: 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;

then (vertices p) \ {v2} c= U by A5;

hence p is_orientedpath_of v1,v2,U by A4, GRAPH_5:def 4; :: thesis: verum

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 that

A1: the carrier of G = U \/ V and

A2: v1 in U and

A3: 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 ) and

A4: 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;

A5: now :: thesis: vertices p c= U

(vertices p) \ {v2} c= vertices p
by XBOOLE_1:36;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

A6: i + 1 <= len p and

A7: not vertices (p /. (i + 1)) c= U and

A8: len q = i and

A9: p = q ^ r and

A10: vertices q c= U by GRAPH_5:20;

A11: p . (i + 1) in the carrier' of G by A6, Th2, NAT_1:12;

p /. (i + 1) = p . (i + 1) by A6, FINSEQ_4:15, NAT_1:12;

then A12: vertices (p /. (i + 1)) = {( the Source of G . (p . (i + 1))),( the Target of G . (p . (i + 1)))} by GRAPH_5:def 1;

then reconsider vy = the Target of G . (p . (i + 1)) as Vertex of G by A6, Lm3;

A15: ( vy in U or vy in V ) by A1, A2, XBOOLE_0:def 3;

end;then consider i being Element of NAT , q, r being FinSequence of the carrier' of G such that

A6: i + 1 <= len p and

A7: not vertices (p /. (i + 1)) c= U and

A8: len q = i and

A9: p = q ^ r and

A10: vertices q c= U by GRAPH_5:20;

A11: p . (i + 1) in the carrier' of G by A6, Th2, NAT_1:12;

p /. (i + 1) = p . (i + 1) by A6, FINSEQ_4:15, NAT_1:12;

then A12: vertices (p /. (i + 1)) = {( the Source of G . (p . (i + 1))),( the Target of G . (p . (i + 1)))} by GRAPH_5:def 1;

A13: now :: thesis: ( the Source of G . (p . (i + 1)) in U implies not the Target of G . (p . (i + 1)) in U )

A14:
1 <= i + 1
by NAT_1:12;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 A12, ZFMISC_1:42;

hence contradiction by A7, XBOOLE_1:7; :: thesis: verum

end;then (vertices (p /. (i + 1))) \/ U = U by A12, ZFMISC_1:42;

hence contradiction by A7, XBOOLE_1:7; :: thesis: verum

then reconsider vy = the Target of G . (p . (i + 1)) as Vertex of G by A6, Lm3;

A15: ( vy in U or vy in V ) by A1, A2, XBOOLE_0:def 3;

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

end;

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

then
the Source of G . (p . (i + 1)) = v1
by A4, GRAPH_5:def 3;

then p . (i + 1) orientedly_joins v1,vy by GRAPH_4:def 1;

hence contradiction by A2, A3, A4, A13, A11, A15, A16, GRAPH_5:def 3; :: thesis: verum

end;then p . (i + 1) orientedly_joins v1,vy by GRAPH_4:def 1;

hence contradiction by A2, A3, A4, A13, A11, A15, A16, GRAPH_5:def 3; :: thesis: verum

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

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

end;hereby :: thesis: verum
end;

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

end;

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

p . (i + 1) orientedly_joins vx,vy
by GRAPH_4:def 1;

hence contradiction by A3, A6, A14, A13, A15, A18, Th2; :: thesis: verum

end;hence contradiction by A3, A6, A14, A13, A15, A18, Th2; :: thesis: verum

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

A20:
i < len p
by A6, NAT_1:13;

A21: i >= 1 + 0 by A17, INT_1:7;

then reconsider vq = the Target of G . (q . i) as Vertex of G by A8, Lm3;

A22: vq in vertices q by A8, A21, Lm4;

the Target of G . (q . i) = the Target of G . (p . i) by A8, A9, A21, Lm1

.= the Source of G . (p . (i + 1)) by A21, A20, GRAPH_1:def 15 ;

hence contradiction by A10, A19, A22; :: thesis: verum

end;A21: i >= 1 + 0 by A17, INT_1:7;

then reconsider vq = the Target of G . (q . i) as Vertex of G by A8, Lm3;

A22: vq in vertices q by A8, A21, Lm4;

the Target of G . (q . i) = the Target of G . (p . i) by A8, A9, A21, Lm1

.= the Source of G . (p . (i + 1)) by A21, A20, GRAPH_1:def 15 ;

hence contradiction by A10, A19, A22; :: thesis: verum

then (vertices p) \ {v2} c= U by A5;

hence p is_orientedpath_of v1,v2,U by A4, GRAPH_5:def 4; :: thesis: verum