let V, U be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: p is_orientedpath_of v1,v2,U
(vertices p) \ {v2} c= V by A1, Def4;
then A3: (vertices p) \ {v2} c= U by A2, XBOOLE_1:1;
p is_orientedpath_of v1,v2 by A1, Def4;
hence p is_orientedpath_of v1,v2,U by A3, Def4; :: thesis: verum