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