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 holds
( v1 in vertices p & v2 in vertices p )
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 holds
( v1 in vertices p & v2 in vertices p )
let p be oriented Chain of G; :: thesis: ( p is_orientedpath_of v1,v2 implies ( v1 in vertices p & v2 in vertices p ) )
assume p is_orientedpath_of v1,v2 ; :: thesis: ( v1 in vertices p & v2 in vertices p )
then A1: ( p <> {} & the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by Def3;
then 1 <= len p by FINSEQ_1:28;
then ( 1 in dom p & len p in dom p ) by FINSEQ_3:27;
hence ( v1 in vertices p & v2 in vertices p ) by A1, Th28; :: thesis: verum