let V, U be set ; for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds
p is_orientedpath_of v1,v2,U
let G be Graph; for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds
p is_orientedpath_of v1,v2,U
let v1, v2 be Element of G; for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds
p is_orientedpath_of v1,v2,U
let p be oriented Chain of G; ( p is_orientedpath_of v1,v2,V & V c= U implies p is_orientedpath_of v1,v2,U )
assume that
A1:
p is_orientedpath_of v1,v2,V
and
A2:
V c= U
; p is_orientedpath_of v1,v2,U
(vertices p) \ {v2} c= V
by A1;
then A3:
(vertices p) \ {v2} c= U
by A2;
p is_orientedpath_of v1,v2
by A1;
hence
p is_orientedpath_of v1,v2,U
by A3; verum