set e = the Element of Edges_At (v,X);
set IT = { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

let x be object ; :: thesis:
assume x in { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ; :: thesis:
then ex c being Element of X * st
( x = c & c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) ;
hence x is FinSequence of the carrier' of G ; :: thesis:

end;

then ( the Element of Edges_At (v,X) in X & the Target of G . the Element of Edges_At (v,X) = v ) by Def1;
hence ex e9 being Element of X st
( the Element of Edges_At (v,X) = e9 & e9 in X & e9 in the carrier' of G & ( v = the Target of G . e9 or v = the Source of G . e9 ) ) by A4; :: thesis:

end;

then ( the Element of Edges_At (v,X) in X & the Source of G . the Element of Edges_At (v,X) = v ) by Def2;
hence ex e9 being Element of X st
( the Element of Edges_At (v,X) = e9 & e9 in X & e9 in the carrier' of G & ( v = the Target of G . e9 or v = the Source of G . e9 ) ) by A5; :: thesis:

end;

then consider e9 being Element of X such that
the Element of Edges_At (v,X) = e9 and
A6: e9 in X and
A7: e9 in the carrier' of G and
A8: ( v = the Target of G . e9 or v = the Source of G . e9 ) ;
reconsider X9 = X as non empty set by A6;
reconsider e9 = e9 as Element of X9 ;
reconsider c = <*e9*> as Element of X * by FINSEQ_1:def 11;
A9: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v )

set s = the Source of G . e9;
reconsider s = the Source of G . e9 as Vertex of G by A7, FUNCT_2:5;
set t = the Target of G . e9;
reconsider t = the Target of G . e9 as Vertex of G by A7, FUNCT_2:5;

end;

end;

c is Path of G by A7, Th4;
then c in { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } by A9;
hence { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } is non empty FinSequenceSet of the carrier' of G by A2, FINSEQ_2:def 3; :: thesis: