let G be Graph; :: thesis: for p being oriented Chain of G
for V being set
for v1, v2 being Vertex of G holds
( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )
let p be oriented Chain of G; :: thesis: for V being set
for v1, v2 being Vertex of G holds
( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )
let V be set ; :: thesis: for v1, v2 being Vertex of G holds
( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )
let v1, v2 be Vertex of G; :: thesis: ( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )
set V9 = V \/ {v2};
thus ( p is_orientedpath_of v1,v2,V implies p is_orientedpath_of v1,v2,V \/ {v2} ) by GRAPH_5:32, XBOOLE_1:7; :: thesis: ( p is_orientedpath_of v1,v2,V \/ {v2} implies p is_orientedpath_of v1,v2,V )
assume A1: p is_orientedpath_of v1,v2,V \/ {v2} ; :: thesis: p is_orientedpath_of v1,v2,V
then (vertices p) \ {v2} c= V \/ {v2} by GRAPH_5:def 4;
then ((vertices p) \ {v2}) \ {v2} c= V by XBOOLE_1:43;
then A2: (vertices p) \ ({v2} \/ {v2}) c= V by XBOOLE_1:41;
p is_orientedpath_of v1,v2 by A1, GRAPH_5:def 4;
hence p is_orientedpath_of v1,v2,V by A2, GRAPH_5:def 4; :: thesis: verum