let G be Graph; :: thesis: for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
let v be Element of G; :: thesis: <*v*> is_oriented_vertex_seq_of {}
set p = <*v*>;
set ec = {} ;
A1: len <*v*> = 0 + 1 by FINSEQ_1:56
.= (len {} ) + 1 ;
for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) ;
hence <*v*> is_oriented_vertex_seq_of {} by A1, Def5; :: thesis: verum