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