let V be set ; :: thesis: for G being Graph
for v1, v2 being Element of the carrier of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds
v1 in V
let G be Graph; :: thesis: for v1, v2 being Element of the carrier of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds
v1 in V
let v1, v2 be Element of the carrier of G; :: thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds
v1 in V
let p be oriented Chain of G; :: thesis: ( p is_orientedpath_of v1,v2,V & v1 <> v2 implies v1 in V )
assume A1: ( p is_orientedpath_of v1,v2,V & v1 <> v2 ) ; :: thesis: v1 in V
then A2: (vertices p) \ {v2} c= V by Def4;
A3: not v1 in {v2} by A1, TARSKI:def 1;
p is_orientedpath_of v1,v2 by A1, Def4;
then v1 in vertices p by Th33;
then v1 in (vertices p) \ {v2} by A3, XBOOLE_0:def 5;
hence v1 in V by A2; :: thesis: verum